Global Talk Keyword Index

GLOBAL TALK KEYWORD INDEX

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

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

A
abstraction	(ARCADE 2021) Relevance and Abstraction
accessibility	(ThEdu'21) Make Isabelle Accessible!
ACL2s	(ThEdu'21) Automated Grading of Automata with ACL2s
Array-based transitions systems	(CADE-28) Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
Asymptotically-tight	(WST 2021) Efficient Computation of Polynomial Resource Bounds for Bounded-Loop Programs
ATP	(ThEdu'21) Learning Theorem Proving by Example - Implementing JavaRes (CADE-28) The CADE-28 ATP System Competition (CASC-28) Results (CADE-28) Law, Morality, Religion, and ATP (ARCADE 2021) The Expansion, Modernisation, and Future of the TPTP World
ATP System	(CADE-28) 17 Ways to make an ATP System Fast
Attestation logics	(CADE-28) Proof Search and Certificates for Evidential Transactions
Automated Deduction	(LFMTP 2021) Automating Induction by Reflection
Automated Deduction in Geometry	(ThEdu'21) Four Geometry Problems to Introduce Automated Deduction in Secondary Schools
Automated First-Order Theorem Proving	(CADE-28) Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
automated geometry proving	(ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
Automated grading	(ThEdu'21) Automated Grading of Automata with ACL2s
Automated Induction	(LFMTP 2021) Automating Induction by Reflection
automated reasoning	(PxTP-7) Alethe: Towards a Generic SMT Proof Format (Extended Abstract) (ThEdu'21) Automated Discovery of Geometrical Theorems in GeoGebra (CADE-28) Confidences for Commonsense Reasoning (CADE-28) Integer Induction in Saturation (LFMTP 2021) Automating Induction by Reflection
automated theorem proving	(CADE-28) A Unifying Splitting Framework (CADE-28) Twee: an equational theorem prover (System Description)
Automatic Complexity Analysis	(WST 2021) Analyzing Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
Automatic feedback	(ThEdu'21) Automated Grading of Automata with ACL2s
automatic theorem provers	(CADE-28) Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
automatic theorem proving	(PxTP-7) General Automation in Coq through Modular Transformations
automatic-theorem-prover	(ARCADE 2021) On Evaluating Theorem Provers
avatar	(CADE-28) A Unifying Splitting Framework
Award	(CADE-28) 2020 Herbrand Award (CADE-28) 2021 Herbrand Award
Awards	(CADE-28) Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
Axiomatic Theories of Truth	(LFMTP 2021) Automating Induction by Reflection
B
bana-comon	(LFMTP 2021) Foundations of the Squirrel meta-logic for reasoning over security protocols
Basic Paramodulation	(CADE-28) Equational Theorem Proving Modulo
Best Papers	(CADE-28) Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
Bill McCune	(CADE-28) Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
binary decision diagram	(CADE-28) Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver
Bounded Model Checking	(ThEdu'21) Automated Instantiation of Control Flow Tracing Exercises
Break 1	(CADE-28) Break
Break 2	(CADE-28) Break
Break 3	(CADE-28) Break
C
C Programs	(WST 2021) Modular Termination Analysis of C Programs
CADE	(ARCADE 2021) Management of the TPTP Problem Set
Case Analysis	(LFMTP 2021) Adelfa: A System for Reasoning about LF Specifications
ccsa	(LFMTP 2021) Foundations of the Squirrel meta-logic for reasoning over security protocols
CDCL	(CADE-28) The ksmt calculus is a delta-complete decision procedure for non-linear constraints
CDSAT	(PxTP-7) Proof Generation in CDSAT
certificate	(PxTP-7) A Framework for Proof-Carrying Logical Transformations
Chromium	(ThEdu'21) Make Isabelle Accessible!
clause selection	(CADE-28) Improving ENIGMA-Style Clause Selection While Learning From History
Closed Forms	(WST 2021) Polynomial Loops: Termination and Beyond
Cloud	(PDAR-21) Constraint Solving in the Serverless Cloud
CNF	(PxTP-7) Reasoning in Many Logics with Vampire: Everything's CNF in the End
collatz conjecture	(CADE-28) An Automated Approach to the Collatz Conjecture (WST 2021) Mixed Base Rewriting for the Collatz Conjecture
Combination	(CADE-28) Unification, Combination, Description Logics, and All That
commonsense reasoning	(CADE-28) Confidences for Commonsense Reasoning
Competition	(CADE-28) The CADE-28 ATP System Competition (CASC-28) Results (CADE-28) Termination and Complexity Competition Results (ARCADE 2021) On Evaluating Theorem Provers
completeness	(CADE-28) Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance (CADE-28) A Unifying Splitting Framework
complexity	(CADE-28) Termination and Complexity Competition Results (ARCADE 2021) Search Spaces for Theorem Proving Strategies
Complexity Analysis	(WST 2021) Polynomial Loops: Termination and Beyond (WST 2021) Parallel Complexity of Term Rewriting Systems
Compliance	(CADE-28) Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes
computational complexity	(CADE-28) Tableau-based decision procedure for non-Fregean logic of sentential identity
computational model	(LFMTP 2021) Foundations of the Squirrel meta-logic for reasoning over security protocols
computer-assisted mathematics	(CADE-28) An Automated Approach to the Collatz Conjecture (WST 2021) Mixed Base Rewriting for the Collatz Conjecture
Condensed Detachment	(CADE-28) Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Connection Method	(CADE-28) Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Constraint	(PDAR-21) Constraint Solving in the Serverless Cloud
contexts	(LFMTP 2021) Interacting safely with an unsafe environment
Coq	(PxTP-7) General Automation in Coq through Modular Transformations (PxTP-7) Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract) (LFMTP 2021) SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts (LFMTP 2021) Countability of Inductive Types Formalized in the Object-Logic Level (LFMTP 2021) The MetaCoq Project (WST 2021) Formalizing Higher-Order Termination in Coq
COQ plugin	(PxTP-7) Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract)
countable	(LFMTP 2021) Countability of Inductive Types Formalized in the Object-Logic Level
Counter-example generation	(ThEdu'21) Automated Grading of Automata with ACL2s
D
Darkside	(CADE-28) Step into the Darkside - Non-classical Logics
Datalog	(LFMTP 2021) Towards a Semantic Framework for Policy Exchange in the Internet
Decidability of Termination	(WST 2021) Polynomial Loops: Termination and Beyond
decision procedure	(CADE-28) Tableau-based decision procedure for non-Fregean logic of sentential identity
deductive verification	(PxTP-7) A Framework for Proof-Carrying Logical Transformations
deep inference	(CADE-28) Subformula Linking for Intuitionistic Logic and Type Theory
defeasible deontic logic	(CADE-28) A Normative Supervisor for Reinforcement Learning Agents (System Description)
delta-complete decision procedures	(CADE-28) The ksmt calculus is a delta-complete decision procedure for non-linear constraints
dependent type	(LFMTP 2021) Countability of Inductive Types Formalized in the Object-Logic Level
dependent type theory	(CADE-28) Subformula Linking for Intuitionistic Logic and Type Theory
derivational complexity	(WST 2021) Between Derivational and Runtime Complexity
Description Logic	(CADE-28) Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes (CADE-28) The Fusemate Logic Programming System (System Description)
Description Logics	(CADE-28) Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (CADE-28) Unification, Combination, Description Logics, and All That
deVrijer’s proof	(WST 2021) deVrijer’s Measure for SN of λ→ in Scheme
diagrams	(CADE-28) Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
discovery	(ThEdu'21) Automated Discovery of Geometrical Theorems in GeoGebra
Disjunctive	(WST 2021) Efficient Computation of Polynomial Resource Bounds for Bounded-Loop Programs
domain-specific language	(CADE-28) Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
DSL	(CADE-28) Automatically Building Diagrams for Olympiad Geometry Problems (System Description) (LFMTP 2021) A logical framework with a graph meta-language
dynamic geometry software	(ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
Dynamic Geometry Systems	(ThEdu'21) Four Geometry Problems to Introduce Automated Deduction in Secondary Schools
E
Edinburgh Logical Framework	(LFMTP 2021) Adelfa: A System for Reasoning about LF Specifications
Education	(ThEdu'21) Automated Instantiation of Control Flow Tracing Exercises
EL	(CADE-28) Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes
Elektron	(ThEdu'21) Make Isabelle Accessible!
elimination	(ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
entailment problems	(CADE-28) Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Equational Reasoning	(CADE-28) Equational Theorem Proving Modulo
Equational Theorem Proving	(CADE-28) Equational Theorem Proving Modulo
estimating probability	(CADE-28) Confidences for Commonsense Reasoning
Euclidean planar geometry	(ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
evaluation	(ARCADE 2021) On Evaluating Theorem Provers
Exercise Generation	(ThEdu'21) Automated Instantiation of Control Flow Tracing Exercises
Expected Runtimes	(WST 2021) Analyzing Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
Expected Sizes	(WST 2021) Analyzing Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
Explanations	(CADE-28) Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
explicit	(ThEdu'21) Evolution of SASyLF 2008-2021
external prover	(PxTP-7) Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract)
F
Facilitating	(LFMTP 2021) Facilitating Meta-Theory Reasoning
Fast	(CADE-28) 17 Ways to make an ATP System Fast
first-class Booleans	(CADE-28) Superposition with First-Class Booleans and Inprocessing Clausification
first-order logic	(PxTP-7) General Automation in Coq through Modular Transformations
first-order resolution	(CADE-28) Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
first-order theorem proving	(CADE-28) Integer Induction in Saturation
Formal Mathematics	(CADE-28) The Isabelle/Naproche Natural Language Proof Assistant (System Description)
formal methods	(PxTP-7) A Framework for Proof-Carrying Logical Transformations
formal proof	(PxTP-7) Alethe: Towards a Generic SMT Proof Format (Extended Abstract)
Formal proofs	(ThEdu'21) A Drag-and-Drop Proof Tactic
formal verification	(CADE-28) Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning (LFMTP 2021) SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts
formalization	(LFMTP 2021) Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style (WST 2021) Formalizing Higher-Order Termination in Coq
Functional Programming	(CADE-28) The Lean 4 Theorem Prover and Programming Language (System Description)
G
GATP	(ThEdu'21) Towards Next Step Guidance in Triangle Construction Problems
Generation	(PxTP-7) Proof Generation in CDSAT
GeoGebra	(ThEdu'21) Automated Discovery of Geometrical Theorems in GeoGebra (ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
geometric inequality	(ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
geometry	(ThEdu'21) Towards Next Step Guidance in Triangle Construction Problems (CADE-28) Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Geometry automated theorem provers	(ThEdu'21) Four Geometry Problems to Introduce Automated Deduction in Secondary Schools
GPU	(PDAR-21) GPU SAT Solving
graph	(LFMTP 2021) A logical framework with a graph meta-language
graph convolutional network	(CADE-28) Neural Precedence Recommender
Guidance	(PDAR-21) Parallel Tricks for Speedy Learned Guidance
H
Hacking	(PDAR-21) Hacking Shared Memory Parallelism in Vampire
Halting Problem	(WST 2021) Did Turing Care of the Halting Problem? (WST 2021) Polynomial Loops: Termination and Beyond
hard typing	(LFMTP 2021) Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
Herbrand	(CADE-28) 2020 Herbrand Award (CADE-28) 2021 Herbrand Award
Heuristics	(CADE-28) Making Higher-Order Superposition Work
higher-order logic	(ThEdu'21) Prooftoys: a Proof Assistant for Beginners (CADE-28) Making Higher-Order Superposition Work (CADE-28) Superposition for Full Higher-Order Logic
Higher-order Pattern Unification	(LFMTP 2021) Adelfa: A System for Reasoning about LF Specifications
higher-order rewriting	(WST 2021) Formalizing Higher-Order Termination in Coq
Hyper tableau	(CADE-28) The Fusemate Logic Programming System (System Description)
I
IDE	(ThEdu'21) Evolution of SASyLF 2008-2021
IMO Grand Challenge	(CADE-28) Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Implementation	(CADE-28) The Fusemate Logic Programming System (System Description)
Implicational Logic	(CADE-28) Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
induction	(CADE-28) Integer Induction in Saturation (LFMTP 2021) Automating Induction by Reflection
inductive definitions	(CADE-28) Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Inductive Reasoning	(LFMTP 2021) Adelfa: A System for Reasoning about LF Specifications
inductive type	(LFMTP 2021) Countability of Inductive Types Formalized in the Object-Logic Level
Inference	(PDAR-21) Parallel Probabilistic Inference
inprocessing clausification	(CADE-28) Superposition with First-Class Booleans and Inprocessing Clausification
integer induction	(CADE-28) Integer Induction in Saturation
integer programming	(PxTP-7) Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
Integrity constraints	(LFMTP 2021) Towards a Semantic Framework for Policy Exchange in the Internet
Interactive Proof Assistant	(CADE-28) The Isabelle/Naproche Natural Language Proof Assistant (System Description)
interactive theorem proving	(PxTP-7) General Automation in Coq through Modular Transformations (CADE-28) Isabelle's Metalogic: Formalization and Proof Checker (CADE-28) Subformula Linking for Intuitionistic Logic and Type Theory (CADE-28) Harpoon: Mechanizing Metatheory Interactively (System Description)
Internet routing	(LFMTP 2021) Towards a Semantic Framework for Policy Exchange in the Internet
Interpretation Methods	(CADE-28) Multi-Dimensional Interpretation Methods for Termination of Term Rewriting
interpreted Boolean type	(CADE-28) Superposition with First-Class Booleans and Inprocessing Clausification
intuitionistic logic	(ThEdu'21) Teaching Intuitionistic Propositional Logic Using Isabelle (CADE-28) Subformula Linking for Intuitionistic Logic and Type Theory
Intuitionistic Propositional Logic	(CADE-28) Efficient SAT-based proof search in Intuitionistic Propositional Logic
isabelle	(CADE-28) Isabelle's Metalogic: Formalization and Proof Checker
Isabelle Proof Assistant	(ThEdu'21) Teaching Intuitionistic Propositional Logic Using Isabelle
Isabelle/VSCode	(ThEdu'21) Make Isabelle Accessible!
ITP	(CADE-28) The Lean 4 Theorem Prover and Programming Language (System Description)
J
JavaRes	(ThEdu'21) Learning Theorem Proving by Example - Implementing JavaRes
K
Knuth-Bendix completion	(CADE-28) Twee: an equational theorem prover (System Description)
L
labelled tableaux	(CADE-28) Tableau-based decision procedure for non-Fregean logic of sentential identity
Lace	(PDAR-21) Demonstrating Work-stealing with Lace and its Application in Sylvan
lambda-calculus	(LFMTP 2021) Interacting safely with an unsafe environment
Law	(CADE-28) Law, Morality, Religion, and ATP
Learned	(PDAR-21) Parallel Tricks for Speedy Learned Guidance
Learning	(CADE-28) Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Lemmas	(CADE-28) Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Linear constraint loops	(WST 2021) Loops for which Multiphase-Linear Ranking Functions are Sufficient
LLVM	(WST 2021) Modular Termination Analysis of C Programs
Local Tracing	(PDAR-21) The Networked Uncertainty Principle, or How I Stopped Worrying and Love Local Tracing
Logic	(ThEdu'21) Learning Theorem Proving by Example - Implementing JavaRes (ThEdu'21) A Drag-and-Drop Proof Tactic (LFMTP 2021) Automating Induction by Reflection
Logic programming	(CADE-28) The Fusemate Logic Programming System (System Description) (WST 2021) Observing Loopingness
logical framework	(LFMTP 2021) A logical framework with a graph meta-language
Logical Frameworks	(CADE-28) Harpoon: Mechanizing Metatheory Interactively (System Description) (LFMTP 2021) Interacting safely with an unsafe environment
logical relation	(LFMTP 2021) Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
logical transformation	(PxTP-7) A Framework for Proof-Carrying Logical Transformations
logical transformations	(PxTP-7) General Automation in Coq through Modular Transformations
Logics	(PxTP-7) Reasoning in Many Logics with Vampire: Everything's CNF in the End (CADE-28) Step into the Darkside - Non-classical Logics
Loop	(WST 2021) Observing Loopingness
M
machine learning	(CADE-28) Neural Precedence Recommender (CADE-28) Improving ENIGMA-Style Clause Selection While Learning From History
many-one reduction	(CADE-28) Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Mathematica	(ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
Mathematical Induction	(LFMTP 2021) Automating Induction by Reflection
mathematical software	(ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
mathematics education	(ThEdu'21) Prooftoys: a Proof Assistant for Beginners (ThEdu'21) Make Isabelle Accessible!
mathematics for engineers	(ThEdu'21) Make Isabelle Accessible!
matrix interpretations	(CADE-28) An Automated Approach to the Collatz Conjecture (WST 2021) Mixed Base Rewriting for the Collatz Conjecture
Mechanizing Meta-Theory	(CADE-28) Harpoon: Mechanizing Metatheory Interactively (System Description)
Meeting	(CADE-28) Newbie's Meeting Place
Meta Level Reasoning	(LFMTP 2021) Automating Induction by Reflection
meta logic	(LFMTP 2021) Countability of Inductive Types Formalized in the Object-Logic Level
meta-logic	(LFMTP 2021) Foundations of the Squirrel meta-logic for reasoning over security protocols
Meta-Theory	(LFMTP 2021) Facilitating Meta-Theory Reasoning
MetaCoq	(LFMTP 2021) The MetaCoq Project
metalogic	(CADE-28) Isabelle's Metalogic: Formalization and Proof Checker
Modal Logics	(CADE-28) Efficient Local Reductions to Basic Modal Logic
Model computation	(CADE-28) The Fusemate Logic Programming System (System Description)
Model construction	(CADE-28) Efficient SAT-based proof search in Intuitionistic Propositional Logic
models	(CADE-28) Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
modularity	(LFMTP 2021) Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style (WST 2021) Modular Termination Analysis of C Programs
Morality	(CADE-28) Law, Morality, Religion, and ATP
Multiphase-linear ranking functions	(WST 2021) Loops for which Multiphase-Linear Ranking Functions are Sufficient
Multivariate	(WST 2021) Efficient Computation of Polynomial Resource Bounds for Bounded-Loop Programs
N
Natural Language Processing	(CADE-28) The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Nelson-Openn	(CADE-28) Politeness and Stable Infiniteness: Stronger Together
Networked	(PDAR-21) The Networked Uncertainty Principle, or How I Stopped Worrying and Love Local Tracing
Newbie	(CADE-28) Newbie's Meeting Place
next step guidance	(ThEdu'21) Towards Next Step Guidance in Triangle Construction Problems
Nipkow	(CADE-28) Isabelle: Growing and Applying a Proof Assistant
Node.js	(ThEdu'21) Make Isabelle Accessible!
Non-classical	(CADE-28) Step into the Darkside - Non-classical Logics
non-Fregean logics	(CADE-28) Tableau-based decision procedure for non-Fregean logic of sentential identity
non-linear constraint solving	(CADE-28) The ksmt calculus is a delta-complete decision procedure for non-linear constraints
non-linear real arithemic	(ARCADE 2021) Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Non-Termination	(WST 2021) Observing Loopingness
Normal Forms	(CADE-28) Efficient Local Reductions to Basic Modal Logic
normative reasoning	(CADE-28) A Normative Supervisor for Reinforcement Learning Agents (System Description)
O
object logic	(LFMTP 2021) Countability of Inductive Types Formalized in the Object-Logic Level
olympiad	(CADE-28) Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Opening	(CADE-28) Reception Opening
Optimizations	(CADE-28) Making Higher-Order Superposition Work
Order-Sorted Algebras	(CADE-28) Multi-Dimensional Interpretation Methods for Termination of Term Rewriting
P
Parallel	(PDAR-21) Parallel Probabilistic Inference (PDAR-21) Parallel Tricks for Speedy Learned Guidance
parallelism	(PDAR-21) Hacking Shared Memory Parallelism in Vampire (WST 2021) Parallel Complexity of Term Rewriting Systems
Parametric Systems	(CADE-28) Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
Place	(CADE-28) Newbie's Meeting Place
Policy based routing	(LFMTP 2021) Towards a Semantic Framework for Policy Exchange in the Internet
Polite Combination	(CADE-28) Politeness and Stable Infiniteness: Stronger Together
Polynomial bounds	(WST 2021) Efficient Computation of Polynomial Resource Bounds for Bounded-Loop Programs
Polynomial Loops	(WST 2021) Polynomial Loops: Termination and Beyond
polynomial termination	(WST 2021) Polynomial Termination over N is Undecidable
polynomials	(CADE-28) The ksmt calculus is a delta-complete decision procedure for non-linear constraints
Positive Almost Sure Termination	(WST 2021) Analyzing Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
Probabilistic	(PDAR-21) Parallel Probabilistic Inference
Probabilistic Integer Programs	(WST 2021) Analyzing Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
Project	(LFMTP 2021) The MetaCoq Project
projective geometry	(PxTP-7) Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract)
Proof	(PxTP-7) Proof Generation in CDSAT
proof assistant	(ThEdu'21) Prooftoys: a Proof Assistant for Beginners (LFMTP 2021) A logical framework with a graph meta-language (LFMTP 2021) Adelfa: A System for Reasoning about LF Specifications
Proof assistants	(ThEdu'21) A Drag-and-Drop Proof Tactic (CADE-28) Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Proof automation	(CADE-28) Verified interactive computation of definite integrals
proof certificates	(PxTP-7) Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
proof checking	(CADE-28) Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver
proof explanation	(CADE-28) Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
proof logging	(PxTP-7) Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
Proof procedures	(CADE-28) The Lean 4 Theorem Prover and Programming Language (System Description)
proof reconstruction	(CADE-28) Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Proof Representations	(CADE-28) Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Proof search	(CADE-28) Proof Search and Certificates for Evidential Transactions (CADE-28) Efficient SAT-based proof search in Intuitionistic Propositional Logic
proof strategy	(LFMTP 2021) A logical framework with a graph meta-language
proof tactic	(LFMTP 2021) A logical framework with a graph meta-language
proof terms	(CADE-28) Isabelle's Metalogic: Formalization and Proof Checker
Proofs	(CADE-28) Non-Clausal Redundancy Properties (CADE-28) Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
Property based testing	(ThEdu'21) Automated Grading of Automata with ACL2s
Propositional Logic	(ThEdu'21) Teaching Intuitionistic Propositional Logic Using Isabelle
Prover	(CADE-28) How can Anyone Trust a Theorem Prover?
pseudo-Boolean	(PxTP-7) Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
PyRes	(ThEdu'21) Learning Theorem Proving by Example - Implementing JavaRes
Q
QEPCAD B	(ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
quantified Boolean formula	(CADE-28) Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver
R
real quantifier elimination	(ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
Reasoning	(PxTP-7) Reasoning in Many Logics with Vampire: Everything's CNF in the End (LFMTP 2021) Facilitating Meta-Theory Reasoning
Reception	(CADE-28) Reception Opening
Recursion	(WST 2021) Modular Termination Analysis of C Programs
recursive neural networks	(CADE-28) Improving ENIGMA-Style Clause Selection While Learning From History
Redundancy	(CADE-28) Non-Clausal Redundancy Properties
Reflection	(LFMTP 2021) Automating Induction by Reflection
refutational completeness	(CADE-28) Superposition with First-Class Booleans and Inprocessing Clausification (CADE-28) Superposition for Full Higher-Order Logic
reinforcement learning agents	(CADE-28) A Normative Supervisor for Reinforcement Learning Agents (System Description)
relevance	(ARCADE 2021) Relevance and Abstraction
Religion	(CADE-28) Law, Morality, Religion, and ATP
Repair	(CADE-28) Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes
resolution	(ThEdu'21) Learning Theorem Proving by Example - Implementing JavaRes (ARCADE 2021) Search Spaces for Theorem Proving Strategies
resolution method	(CADE-28) Confidences for Commonsense Reasoning
Results	(CADE-28) The CADE-28 ATP System Competition (CASC-28) Results
rewriting	(WST 2021) Parallel Complexity of Term Rewriting Systems
ruler and compass constructions	(ThEdu'21) Towards Next Step Guidance in Triangle Construction Problems
runtime complexity	(WST 2021) Between Derivational and Runtime Complexity
S
SAT	(CADE-28) Non-Clausal Redundancy Properties (PDAR-21) GPU SAT Solving
satisfiability	(PxTP-7) Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
Satisfiability Modulo Theories	(PxTP-7) Alethe: Towards a Generic SMT Proof Format (Extended Abstract) (ThEdu'21) Automated Instantiation of Control Flow Tracing Exercises (CADE-28) Politeness and Stable Infiniteness: Stronger Together
satisfiability solving	(CADE-28) An Automated Approach to the Collatz Conjecture (WST 2021) Mixed Base Rewriting for the Collatz Conjecture
saturation	(CADE-28) Integer Induction in Saturation
saturation-based theorem proving	(CADE-28) Neural Precedence Recommender (CADE-28) Improving ENIGMA-Style Clause Selection While Learning From History
Secondary schools geometry proofs	(ThEdu'21) Four Geometry Problems to Introduce Automated Deduction in Secondary Schools
security protocols	(LFMTP 2021) Foundations of the Squirrel meta-logic for reasoning over security protocols
Sentential Calculus with Identity	(CADE-28) Tableau-based decision procedure for non-Fregean logic of sentential identity
Separation Logic	(CADE-28) Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Sequent calculus	(CADE-28) Proof Search and Certificates for Evidential Transactions
Serverless	(PDAR-21) Constraint Solving in the Serverless Cloud
services	(ARCADE 2021) The Expansion, Modernisation, and Future of the TPTP World
set of support	(CADE-28) Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
Shared Memory	(PDAR-21) Hacking Shared Memory Parallelism in Vampire
Simplification	(CADE-28) Equational Theorem Proving Modulo
simplification ordering	(CADE-28) Neural Precedence Recommender
Simply typed lambda calculus	(WST 2021) deVrijer’s Measure for SN of λ→ in Scheme
Skolem	(CADE-28) Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
SML	(LFMTP 2021) SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts
SMT	(CADE-28) Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning (ARCADE 2021) Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
SMT solvers	(CADE-28) The ksmt calculus is a delta-complete decision procedure for non-linear constraints
SMT solving	(CADE-28) Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
soft typing	(LFMTP 2021) Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
Solving	(PDAR-21) GPU SAT Solving (PDAR-21) Constraint Solving in the Serverless Cloud
SOS	(CADE-28) Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
splitting	(CADE-28) A Unifying Splitting Framework
static analysis	(WST 2021) Between Derivational and Runtime Complexity
string rewriting	(CADE-28) An Automated Approach to the Collatz Conjecture (WST 2021) Mixed Base Rewriting for the Collatz Conjecture
Strong normalization	(WST 2021) deVrijer’s Measure for SN of λ→ in Scheme
Structural Induction	(LFMTP 2021) Automating Induction by Reflection
subformula linking	(CADE-28) Subformula Linking for Intuitionistic Logic and Type Theory
SUMO	(ThEdu'21) Learning Theorem Proving by Example - Implementing JavaRes
superposition	(CADE-28) Superposition with First-Class Booleans and Inprocessing Clausification (CADE-28) Making Higher-Order Superposition Work (CADE-28) Superposition for Full Higher-Order Logic
Sylvan	(PDAR-21) Demonstrating Work-stealing with Lace and its Application in Sylvan
symbol precedence	(CADE-28) Neural Precedence Recommender
Symbolic Execution	(WST 2021) Modular Termination Analysis of C Programs
Symbolic integration	(CADE-28) Verified interactive computation of definite integrals
system description	(CADE-28) Twee: an equational theorem prover (System Description)
T
Tactics	(ThEdu'21) A Drag-and-Drop Proof Tactic
Tarski	(ThEdu'21) Symbolic Comparison of Geometric Quantities in GeoGebra
TBA	(CADE-28) Isabelle: Growing and Applying a Proof Assistant
TBA1	(ThEdu'21) How can we make Formal Proof Teachable?
TBA2	(ThEdu'21) How can we make Formal Proof Teachable?
TBA3	(ThEdu'21) How can we make Formal Proof Teachable?
Techniques	(CADE-28) Making Higher-Order Superposition Work
term rewriting	(CADE-28) Multi-Dimensional Interpretation Methods for Termination of Term Rewriting (WST 2021) Polynomial Termination over N is Undecidable (WST 2021) Between Derivational and Runtime Complexity
Term Rewriting Systems	(WST 2021) Observing Loopingness
termination	(CADE-28) Multi-Dimensional Interpretation Methods for Termination of Term Rewriting (CADE-28) Tableau-based decision procedure for non-Fregean logic of sentential identity (CADE-28) An Automated Approach to the Collatz Conjecture (CADE-28) Termination and Complexity Competition Results (WST 2021) Mixed Base Rewriting for the Collatz Conjecture (WST 2021) Formalizing Higher-Order Termination in Coq (WST 2021) Did Turing Care of the Halting Problem?
Termination analysis	(WST 2021) Modular Termination Analysis of C Programs (WST 2021) Loops for which Multiphase-Linear Ranking Functions are Sufficient
The 2020	(CADE-28) 2020 Herbrand Award
The 2021	(CADE-28) 2021 Herbrand Award
Theorem	(CADE-28) How can Anyone Trust a Theorem Prover?
theorem prover	(PxTP-7) A Framework for Proof-Carrying Logical Transformations (CADE-28) The Lean 4 Theorem Prover and Programming Language (System Description) (LFMTP 2021) A logical framework with a graph meta-language
theorem proving	(ThEdu'21) Make Isabelle Accessible! (CADE-28) Efficient Local Reductions to Basic Modal Logic (CADE-28) A Normative Supervisor for Reinforcement Learning Agents (System Description) (ARCADE 2021) Management of the TPTP Problem Set (ARCADE 2021) Relevance and Abstraction (ARCADE 2021) Search Spaces for Theorem Proving Strategies
Theory Combination	(CADE-28) Politeness and Stable Infiniteness: Stronger Together
Theory of Computation	(ThEdu'21) Automated Grading of Automata with ACL2s
Tobias	(CADE-28) Isabelle: Growing and Applying a Proof Assistant
Topical	(CADE-28) Reception Opening
TPTP	(ThEdu'21) Learning Theorem Proving by Example - Implementing JavaRes
TPTP problem set	(ARCADE 2021) Management of the TPTP Problem Set
TPTP World	(ARCADE 2021) The Expansion, Modernisation, and Future of the TPTP World
Tracing	(ThEdu'21) Automated Instantiation of Control Flow Tracing Exercises
transcendental functions	(CADE-28) The ksmt calculus is a delta-complete decision procedure for non-linear constraints
translation	(LFMTP 2021) Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
Trust	(CADE-28) How can Anyone Trust a Theorem Prover?
Truth Predicate	(LFMTP 2021) Automating Induction by Reflection
Turing machines	(WST 2021) Did Turing Care of the Halting Problem?
type systems	(ThEdu'21) Evolution of SASyLF 2008-2021
type theory	(LFMTP 2021) Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style
Typescript	(ThEdu'21) Make Isabelle Accessible!
U
uncertain reasoning	(CADE-28) Confidences for Commonsense Reasoning
Uncertainty Principle	(PDAR-21) The Networked Uncertainty Principle, or How I Stopped Worrying and Love Local Tracing
undecidability	(WST 2021) Polynomial Termination over N is Undecidable
Unification	(CADE-28) Unification, Combination, Description Logics, and All That
unit equality	(CADE-28) Twee: an equational theorem prover (System Description)
unsatisfiability proofs	(ARCADE 2021) Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
user interface	(ThEdu'21) Prooftoys: a Proof Assistant for Beginners (CADE-28) Verified interactive computation of definite integrals (LFMTP 2021) A logical framework with a graph meta-language
User interfaces	(ThEdu'21) A Drag-and-Drop Proof Tactic
V
Vampire	(PxTP-7) Reasoning in Many Logics with Vampire: Everything's CNF in the End (PDAR-21) Hacking Shared Memory Parallelism in Vampire
W
Ways	(CADE-28) 17 Ways to make an ATP System Fast
Woody Bledsoe	(CADE-28) Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
Work-stealing	(PDAR-21) Demonstrating Work-stealing with Lace and its Application in Sylvan
Worst-case	(WST 2021) Efficient Computation of Polynomial Resource Bounds for Bounded-Loop Programs
Z
Zipperposition	(CADE-28) Superposition with First-Class Booleans and Inprocessing Clausification