Talk Keyword Index

TALK KEYWORD INDEX

This page contains an index consisting of author-provided keywords.

Shortcuts: A B C D E F G H I K L M N O P Q R S T U W

A
algebraic number theory	Formalising the Krull Topology in Lean (Online talk)
annotating proofs	PISE (Proofscape Integrated Study Environment) (Online talk)
ar5iv	Welcome to ar5iv! Wrestling with the Open Problems of Scholarly Writing (Online Talk)
Archive of Formal Proofs	Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs Re-imagining the Isabelle Archive of Formal Proofs (Online Talk)
argument graph	Sophize Mathematics Library (Online talk)
argument mapping	PISE (Proofscape Integrated Study Environment) (Online talk)
arXiv	Welcome to ar5iv! Wrestling with the Open Problems of Scholarly Writing (Online Talk)
Automated Configuration	Targeted Configuration of SMT Solver (Online Talk)
Automated conjecturing	LOL: A library of lemmas for data-driven conjecturing (Online talk)
automated reasoning	Experiments with Automated Reasoning in the Class Learning to Reason Assisted by Automated Reasoning (Online Talk) Lemmaless Induction in Trace Logic (Online Talk)
automated software verification	Lemmaless Induction in Trace Logic (Online Talk)
Automating Formalization	A Parallel Corpus for Natural Language Machine Translation to Isabelle
B
belief set	Sophize Mathematics Library (Online talk)
Branch Cuts	Working with Families of Inverse Functions
C
Centrality metrics	Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs
Change of variables	Formalizing the change of variables formula for integrals in mathlib (Online Talk)
client-server architecture	Python client for Isabelle server (System Entry)
Closure Algebras	Formalising Basic Topology for Computational Logic in Simple Type Theory (Online Talk)
Compactness Theorem	Hall's Theorem for Enumerable Families of Finite Sets (Online Talk)
complex analysis	Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
Complex networks	Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs
computational logic	Experiments with Automated Reasoning in the Class
computer aided teaching	Experiments with Automated Reasoning in the Class
confidential computing	Understanding Trust Assumptions for Attestation in Confidential Computing (Online talk)
Configuration Invention	Targeted Configuration of SMT Solver (Online Talk)
continuum hypothesis	Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
controlled language	Setting up Set-theoretical Foundations in Naproche
controlled natural language	Web-Naproche
Convex Optimisation	Verified Convex Optimization for Hybrid Systems
D
Dataset	An evaluation of NLP methods to extract mathematical token descriptors (Online Talk) Making the Census of Cubic Vertex Transitive Graphs searchable and FAIR (Online Talk)
Decomposition rules	Decomposition Rules: Dynamic, Schematic, Novel Axioms (Online Talk)
Dependency graphs	Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs
Dependent types	Graded rings in Lean's Dependent type theory (Online Talk)
E
extremal combinatorics	Formalising the Kruskal-Katona theorem in Lean (Online talk)
F
FAIR	Making the Census of Cubic Vertex Transitive Graphs searchable and FAIR (Online Talk)
Finite Automata	Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification (Online Talk)
first-order theorem proving	Lemmaless Induction in Trace Logic (Online Talk)
Formal entity network	Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs
formal math	Formalising the Krull Topology in Lean (Online talk)
formal mathematics	Setting up Set-theoretical Foundations in Naproche
Formal Methods	Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification (Online Talk)
formal specification and verification	Understanding Trust Assumptions for Attestation in Confidential Computing (Online talk)
Formal Specifications	Hierarchical Higher-Order Port-graph Rewriting as a Modelling Tool
formal verification	Formalizing Algorithms for Real Quantifier Elimination (Online Talk)
Formalisation	Formalising Nominal AC-Unification (Online talk) Formalising the Kruskal-Katona theorem in Lean (Online talk) Hall's Theorem for Enumerable Families of Finite Sets (Online Talk)
formalisation of mathematics	Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
formalization	Formalizing the change of variables formula for integrals in mathlib (Online Talk) Case Studies on Realms (Online talk) Setting up Set-theoretical Foundations in Naproche
Formalization quality	Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs
G
Galois groups	Formalising the Krull Topology in Lean (Online talk)
generalized set theory	Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
Graded rings	Graded rings in Lean's Dependent type theory (Online Talk)
Graph Rewriting	Hierarchical Higher-Order Port-graph Rewriting as a Modelling Tool
graphs	Making the Census of Cubic Vertex Transitive Graphs searchable and FAIR (Online Talk)
H
Hall's Theorem	Hall's Theorem for Enumerable Families of Finite Sets (Online Talk)
Heat equation	On the Formalization of the Heat Conduction Problem in HOL
Higher-Order Logic	Formalization of Partial Differential Equations in HOL On the Formalization of the Heat Conduction Problem in HOL Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
HOL Light	Formalization of Partial Differential Equations in HOL
Hybrid reasoning	Decomposition Rules: Dynamic, Schematic, Novel Axioms (Online Talk)
Hybrid Systems	Verified Convex Optimization for Hybrid Systems
I
Incremental Reasoning	OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas (Online Talk)
induction	Lemmaless Induction in Trace Logic (Online Talk)
Informal Mathematics	Injecting Formal Mathematics Into LaTeX System Description sTeX3 – A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents
Integral	Formalizing the change of variables formula for integrals in mathlib (Online Talk)
Interactive Theorem Proving	Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification (Online Talk)
Inverse functions	Working with Families of Inverse Functions
Isabelle	Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs Re-imagining the Isabelle Archive of Formal Proofs (Online Talk) Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis Hall's Theorem for Enumerable Families of Finite Sets (Online Talk) Python client for Isabelle server (System Entry) A Parallel Corpus for Natural Language Machine Translation to Isabelle
Isabelle/HOL	Formalising Basic Topology for Computational Logic in Simple Type Theory (Online Talk) Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification (Online Talk)
K
knowledge management services	OEIS Semantified -- A Tetrapodal Data Set
knowledge organization	Sophize Mathematics Library (Online talk)
L
Lambda-Calculus	Hierarchical Higher-Order Port-graph Rewriting as a Modelling Tool
lattice	Case Studies on Realms (Online talk)
Lean	Verified Convex Optimization for Hybrid Systems Graded rings in Lean's Dependent type theory (Online Talk) Formalising the Krull Topology in Lean (Online talk)
Lean theorem prover	Formalising the Kruskal-Katona theorem in Lean (Online talk)
Logic education	Learning to Reason Assisted by Automated Reasoning (Online Talk)
M
Machine Learning	Targeted Configuration of SMT Solver (Online Talk) A Parallel Corpus for Natural Language Machine Translation to Isabelle
Machine Translation	A Parallel Corpus for Natural Language Machine Translation to Isabelle
machine-actionable	OEIS Semantified -- A Tetrapodal Data Set
markdown	Sophize Mathematics Library (Online talk)
MathDataHub	Making the Census of Cubic Vertex Transitive Graphs searchable and FAIR (Online Talk)
Mathematical documents	Welcome to ar5iv! Wrestling with the Open Problems of Scholarly Writing (Online Talk)
Mathematical Knowledge Management	Injecting Formal Mathematics Into LaTeX System Description sTeX3 – A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents An Integrated Web Platform for the Mizar Mathematical Library (Online Talk)
Mathematical langauge processing	An evaluation of NLP methods to extract mathematical token descriptors (Online Talk)
mathlib	Graded rings in Lean's Dependent type theory (Online Talk) Formalizing the change of variables formula for integrals in mathlib (Online Talk) Formalising the Krull Topology in Lean (Online talk)
metamath	Sophize Mathematics Library (Online talk)
Mizar Mathematical Library	An Integrated Web Platform for the Mizar Mathematical Library (Online Talk)
MMT	Case Studies on Realms (Online talk)
N
Naproche	Web-Naproche
Nominal AC-Unification	Formalising Nominal AC-Unification (Online talk)
O
OEIS	OEIS Semantified -- A Tetrapodal Data Set
P
Parallel Corpus	A Parallel Corpus for Natural Language Machine Translation to Isabelle
Partial Differential Equations	Formalization of Partial Differential Equations in HOL On the Formalization of the Heat Conduction Problem in HOL
Paul Erdős	Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
proof graph	Sophize Mathematics Library (Online talk)
proof-generating machine	Sophize Mathematics Library (Online talk)
ProVerif	Understanding Trust Assumptions for Attestation in Confidential Computing (Online talk)
PVS	Formalising Nominal AC-Unification (Online talk)
Python	Python client for Isabelle server (System Entry)
Q
QBF	Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification (Online Talk)
QED manifesto	An Integrated Web Platform for the Mizar Mathematical Library (Online Talk)
QSAT	Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification (Online Talk)
Quantified Boolean Formulas	OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas (Online Talk)
quantifier elimination	Formalizing Algorithms for Real Quantifier Elimination (Online Talk)
Query answering	Decomposition Rules: Dynamic, Schematic, Novel Axioms (Online Talk)
R
Real Algebra	SMT solving for Arithmetic Theories
real arithmetic	Formalizing Algorithms for Real Quantifier Elimination (Online Talk)
realm	Case Studies on Realms (Online talk)
remote attestation	Understanding Trust Assumptions for Attestation in Confidential Computing (Online talk)
S
Satisfiability checking	SMT solving for Arithmetic Theories
Satisfiability Modulo Theories	Targeted Configuration of SMT Solver (Online Talk)
Scholarly HTML5	Welcome to ar5iv! Wrestling with the Open Problems of Scholarly Writing (Online Talk)
semantic data	Sophize Mathematics Library (Online talk)
Semantification	OEIS Semantified -- A Tetrapodal Data Set
Separation of Variables	On the Formalization of the Heat Conduction Problem in HOL
set theory	Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis Setting up Set-theoretical Foundations in Naproche
Simple Type Theory	Formalising Basic Topology for Computational Logic in Simple Type Theory (Online Talk)
Simplification Rules	Working with Families of Inverse Functions
SMT solving	SMT solving for Arithmetic Theories
soft types	Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
Solution Counting	OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas (Online Talk)
Sophize	Sophize Mathematics Library (Online talk)
Sperner	Formalising the Kruskal-Katona theorem in Lean (Online talk)
sTeX	Injecting Formal Mathematics Into LaTeX
Strategies	Hierarchical Higher-Order Port-graph Rewriting as a Modelling Tool
study aids	PISE (Proofscape Integrated Study Environment) (Online talk)
superposition-based proving	Lemmaless Induction in Trace Logic (Online Talk)
Surface Language	Injecting Formal Mathematics Into LaTeX
symbolic security analysis	Understanding Trust Assumptions for Attestation in Confidential Computing (Online talk)
System On TPTP	Web-Naproche
T
Tetrapod	OEIS Semantified -- A Tetrapodal Data Set
TeX	Injecting Formal Mathematics Into LaTeX System Description sTeX3 – A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents
Text summarization	An evaluation of NLP methods to extract mathematical token descriptors (Online Talk)
Theorem Proving	Formalization of Partial Differential Equations in HOL Formalizing Algorithms for Real Quantifier Elimination (Online Talk) On the Formalization of the Heat Conduction Problem in HOL Hall's Theorem for Enumerable Families of Finite Sets (Online Talk) LOL: A library of lemmas for data-driven conjecturing (Online talk)
Theorema	Learning to Reason Assisted by Automated Reasoning (Online Talk)
Theory Exploration	LOL: A library of lemmas for data-driven conjecturing (Online talk)
topology	Formalising Basic Topology for Computational Logic in Simple Type Theory (Online Talk) Case Studies on Realms (Online talk)
typeclasses	Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
U
understanding proofs	PISE (Proofscape Integrated Study Environment) (Online talk)
User Experience	Re-imagining the Isabelle Archive of Formal Proofs (Online Talk)
User Interface	Re-imagining the Isabelle Archive of Formal Proofs (Online Talk)
W
Web service	An Integrated Web Platform for the Mizar Mathematical Library (Online Talk)
webinterface	Web-Naproche