CADE-28: THE 28TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION

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

A
Array-based transitions systems	Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
ATP	The CADE-28 ATP System Competition (CASC-28) Results Law, Morality, Religion, and ATP
ATP System	17 Ways to make an ATP System Fast
Attestation logics	Proof Search and Certificates for Evidential Transactions
Automated First-Order Theorem Proving	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
automated reasoning	Confidences for Commonsense Reasoning Integer Induction in Saturation
automated theorem proving	A Unifying Splitting Framework Twee: an equational theorem prover (System Description)
automatic theorem provers	Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
avatar	A Unifying Splitting Framework
Award	2020 Herbrand Award 2021 Herbrand Award
Awards	Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
B
Basic Paramodulation	Equational Theorem Proving Modulo
Best Papers	Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
Bill McCune	Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
binary decision diagram	Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver
Break 1	Break
Break 2	Break
Break 3	Break
C
CDCL	The ksmt calculus is a delta-complete decision procedure for non-linear constraints
clause selection	Improving ENIGMA-Style Clause Selection While Learning From History
collatz conjecture	An Automated Approach to the Collatz Conjecture
Combination	Unification, Combination, Description Logics, and All That
commonsense reasoning	Confidences for Commonsense Reasoning
Competition	The CADE-28 ATP System Competition (CASC-28) Results Termination and Complexity Competition Results
completeness	Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance A Unifying Splitting Framework
complexity	Termination and Complexity Competition Results
Compliance	Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes
computational complexity	Tableau-based decision procedure for non-Fregean logic of sentential identity
computer-assisted mathematics	An Automated Approach to the Collatz Conjecture
Condensed Detachment	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Connection Method	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
D
Darkside	Step into the Darkside - Non-classical Logics
decision procedure	Tableau-based decision procedure for non-Fregean logic of sentential identity
deep inference	Subformula Linking for Intuitionistic Logic and Type Theory
defeasible deontic logic	A Normative Supervisor for Reinforcement Learning Agents (System Description)
delta-complete decision procedures	The ksmt calculus is a delta-complete decision procedure for non-linear constraints
dependent type theory	Subformula Linking for Intuitionistic Logic and Type Theory
Description Logic	Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes The Fusemate Logic Programming System (System Description)
Description Logics	Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures Unification, Combination, Description Logics, and All That
diagrams	Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
domain-specific language	Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
DSL	Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
E
EL	Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes
entailment problems	Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Equational Reasoning	Equational Theorem Proving Modulo
Equational Theorem Proving	Equational Theorem Proving Modulo
estimating probability	Confidences for Commonsense Reasoning
Explanations	Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
F
Fast	17 Ways to make an ATP System Fast
first-class Booleans	Superposition with First-Class Booleans and Inprocessing Clausification
first-order resolution	Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
first-order theorem proving	Integer Induction in Saturation
Formal Mathematics	The Isabelle/Naproche Natural Language Proof Assistant (System Description)
formal verification	Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
Functional Programming	The Lean 4 Theorem Prover and Programming Language (System Description)
G
geometry	Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
graph convolutional network	Neural Precedence Recommender
H
Herbrand	2020 Herbrand Award 2021 Herbrand Award
Heuristics	Making Higher-Order Superposition Work
higher-order logic	Making Higher-Order Superposition Work Superposition for Full Higher-Order Logic
Hyper tableau	The Fusemate Logic Programming System (System Description)
I
IMO Grand Challenge	Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Implementation	The Fusemate Logic Programming System (System Description)
Implicational Logic	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
induction	Integer Induction in Saturation
inductive definitions	Unifying Decidable Entailments in Separation Logic with Inductive Definitions
inprocessing clausification	Superposition with First-Class Booleans and Inprocessing Clausification
integer induction	Integer Induction in Saturation
Interactive Proof Assistant	The Isabelle/Naproche Natural Language Proof Assistant (System Description)
interactive theorem proving	Isabelle's Metalogic: Formalization and Proof Checker Subformula Linking for Intuitionistic Logic and Type Theory Harpoon: Mechanizing Metatheory Interactively (System Description)
Interpretation Methods	Multi-Dimensional Interpretation Methods for Termination of Term Rewriting
interpreted Boolean type	Superposition with First-Class Booleans and Inprocessing Clausification
intuitionistic logic	Subformula Linking for Intuitionistic Logic and Type Theory
Intuitionistic Propositional Logic	Efficient SAT-based proof search in Intuitionistic Propositional Logic
isabelle	Isabelle's Metalogic: Formalization and Proof Checker
ITP	The Lean 4 Theorem Prover and Programming Language (System Description)
K
Knuth-Bendix completion	Twee: an equational theorem prover (System Description)
L
labelled tableaux	Tableau-based decision procedure for non-Fregean logic of sentential identity
Law	Law, Morality, Religion, and ATP
Learning	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Lemmas	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Logic programming	The Fusemate Logic Programming System (System Description)
Logical Frameworks	Harpoon: Mechanizing Metatheory Interactively (System Description)
Logics	Step into the Darkside - Non-classical Logics
M
machine learning	Neural Precedence Recommender Improving ENIGMA-Style Clause Selection While Learning From History
many-one reduction	Unifying Decidable Entailments in Separation Logic with Inductive Definitions
matrix interpretations	An Automated Approach to the Collatz Conjecture
Mechanizing Meta-Theory	Harpoon: Mechanizing Metatheory Interactively (System Description)
Meeting	Newbie's Meeting Place
metalogic	Isabelle's Metalogic: Formalization and Proof Checker
Modal Logics	Efficient Local Reductions to Basic Modal Logic
Model computation	The Fusemate Logic Programming System (System Description)
Model construction	Efficient SAT-based proof search in Intuitionistic Propositional Logic
models	Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Morality	Law, Morality, Religion, and ATP
N
Natural Language Processing	The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Nelson-Openn	Politeness and Stable Infiniteness: Stronger Together
Newbie	Newbie's Meeting Place
Nipkow	Isabelle: Growing and Applying a Proof Assistant
Non-classical	Step into the Darkside - Non-classical Logics
non-Fregean logics	Tableau-based decision procedure for non-Fregean logic of sentential identity
non-linear constraint solving	The ksmt calculus is a delta-complete decision procedure for non-linear constraints
Normal Forms	Efficient Local Reductions to Basic Modal Logic
normative reasoning	A Normative Supervisor for Reinforcement Learning Agents (System Description)
O
olympiad	Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Opening	Reception Opening
Optimizations	Making Higher-Order Superposition Work
Order-Sorted Algebras	Multi-Dimensional Interpretation Methods for Termination of Term Rewriting
P
Parametric Systems	Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
Place	Newbie's Meeting Place
Polite Combination	Politeness and Stable Infiniteness: Stronger Together
polynomials	The ksmt calculus is a delta-complete decision procedure for non-linear constraints
Proof assistants	Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Proof automation	Verified interactive computation of definite integrals
proof checking	Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver
proof explanation	Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
Proof procedures	The Lean 4 Theorem Prover and Programming Language (System Description)
proof reconstruction	Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Proof Representations	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Proof search	Proof Search and Certificates for Evidential Transactions Efficient SAT-based proof search in Intuitionistic Propositional Logic
proof terms	Isabelle's Metalogic: Formalization and Proof Checker
Proofs	Non-Clausal Redundancy Properties Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
Prover	How can Anyone Trust a Theorem Prover?
Q
quantified Boolean formula	Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver
R
Reception	Reception Opening
recursive neural networks	Improving ENIGMA-Style Clause Selection While Learning From History
Redundancy	Non-Clausal Redundancy Properties
refutational completeness	Superposition with First-Class Booleans and Inprocessing Clausification Superposition for Full Higher-Order Logic
reinforcement learning agents	A Normative Supervisor for Reinforcement Learning Agents (System Description)
Religion	Law, Morality, Religion, and ATP
Repair	Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes
resolution method	Confidences for Commonsense Reasoning
Results	The CADE-28 ATP System Competition (CASC-28) Results
S
SAT	Non-Clausal Redundancy Properties
Satisfiability Modulo Theories	Politeness and Stable Infiniteness: Stronger Together
satisfiability solving	An Automated Approach to the Collatz Conjecture
saturation	Integer Induction in Saturation
saturation-based theorem proving	Neural Precedence Recommender Improving ENIGMA-Style Clause Selection While Learning From History
Sentential Calculus with Identity	Tableau-based decision procedure for non-Fregean logic of sentential identity
Separation Logic	Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Sequent calculus	Proof Search and Certificates for Evidential Transactions
set of support	Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
Simplification	Equational Theorem Proving Modulo
simplification ordering	Neural Precedence Recommender
Skolem	Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
SMT	Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
SMT solvers	The ksmt calculus is a delta-complete decision procedure for non-linear constraints
SMT solving	Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
SOS	Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
splitting	A Unifying Splitting Framework
string rewriting	An Automated Approach to the Collatz Conjecture
subformula linking	Subformula Linking for Intuitionistic Logic and Type Theory
superposition	Superposition with First-Class Booleans and Inprocessing Clausification Making Higher-Order Superposition Work Superposition for Full Higher-Order Logic
symbol precedence	Neural Precedence Recommender
Symbolic integration	Verified interactive computation of definite integrals
system description	Twee: an equational theorem prover (System Description)
T
TBA	Isabelle: Growing and Applying a Proof Assistant
Techniques	Making Higher-Order Superposition Work
term rewriting	Multi-Dimensional Interpretation Methods for Termination of Term Rewriting
termination	Multi-Dimensional Interpretation Methods for Termination of Term Rewriting Tableau-based decision procedure for non-Fregean logic of sentential identity An Automated Approach to the Collatz Conjecture Termination and Complexity Competition Results
The 2020	2020 Herbrand Award
The 2021	2021 Herbrand Award
Theorem	How can Anyone Trust a Theorem Prover?
theorem prover	The Lean 4 Theorem Prover and Programming Language (System Description)
theorem proving	Efficient Local Reductions to Basic Modal Logic A Normative Supervisor for Reinforcement Learning Agents (System Description)
Theory Combination	Politeness and Stable Infiniteness: Stronger Together
Tobias	Isabelle: Growing and Applying a Proof Assistant
Topical	Reception Opening
transcendental functions	The ksmt calculus is a delta-complete decision procedure for non-linear constraints
Trust	How can Anyone Trust a Theorem Prover?
U
uncertain reasoning	Confidences for Commonsense Reasoning
Unification	Unification, Combination, Description Logics, and All That
unit equality	Twee: an equational theorem prover (System Description)
user interface	Verified interactive computation of definite integrals
W
Ways	17 Ways to make an ATP System Fast
Woody Bledsoe	Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
Z
Zipperposition	Superposition with First-Class Booleans and Inprocessing Clausification

Disclaimer | Powered by EasyChair Smart Program