CADE-30: 30TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION

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

(
(ground) first-order logic	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
A
arithmetic	Learning Conjecturing from Scratch
Arrays	What's Decidable About Arrays With Sums?
ATP	Interoperability of Proof systems with SC-TPTP (System Description)
Automated Deduction	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Automated Reasoning	From Modal Sequent Calculi to Modal Resolution
automated theorem proving	Faithful Logic Embeddings in HOL – Deep and Shallow Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories Towards the Verification of Higher-Order Logic Automated Reasoning Premise Selection with the Alternating-Path-Method
B
box folding	Unfolding Boxes with Local Constraints
C
call-by-value	A Fresh Inductive Approach to Useful Call-by-Value Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
Cardinality Constraints	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Certificate	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Classical higher-order logic	Faithful Logic Embeddings in HOL – Deep and Shallow
Clause Selection	Efficient Neural Clause-Selection Reinforcement
common unfoldings	Unfolding Boxes with Local Constraints
Concrete Domains	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Condensed detachment	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Conditional rewriting	Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems
Confluence	Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting
Congruence Closure	Computing Ground Congruence Classes
conjecturing	Learning Conjecturing from Scratch
Constrained Horn Clauses	Infinite State Model Checking by Learning Transitive Relations
Cut Elimination Theorem	Cut Elimination for Negative Free Logics with Definite Descriptions
Cylindrical Algebraic Decomposition	More is Less: Adding Polynomials for Faster Explanations in NLSAT
D
data structure	Verified Path Indexing
Decision procedures	What's Decidable About Arrays With Sums?
Deduktionstreffen	TBA TBA
Deep and shallow logic embeddings	Faithful Logic Embeddings in HOL – Deep and Shallow
Deep Reinforcement Learning	Efficient Neural Clause-Selection Reinforcement
Definite Descriptions	Cut Elimination for Negative Free Logics with Definite Descriptions
Dependency pairs	Lexicographic Combination of Reduction Pairs Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
Derivations	Review of the TPTP format for derivations
Description Logic	Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
Description Logics	Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics
Differential dynamic logic	A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Differential-algebraic equations	A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
E
Enumeration	Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
Equational Reasoning	Anti-pattern templates Computing Ground Congruence Classes
Equational theories	Equational Reasoning Modulo Commutativity in Languages with Binders
Equivalence closure	Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
evaluation strategies	A Fresh Inductive Approach to Useful Call-by-Value
F
Faithfulness	Faithful Logic Embeddings in HOL – Deep and Shallow
First-Order Automated Reasoning	Computing Ground Congruence Classes
first-order reasoning	Premise Selection with the Alternating-Path-Method
Format	Review of the TPTP format for derivations
Formula equations	Computing Witnesses Using the SCAN Algorithm
G
Generalized Term Rewriting Systems	Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems
gentle theory combination	Being polite is not enough (and other limits of theory combination)
Grammar-based tree compression	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Graph acyclicity	Unfolding Boxes with Local Constraints
Graph connectivity	Unfolding Boxes with Local Constraints
H
hierarchical reasoning	On Symbol Elimination and Uniform Interpolation in Theory Extensions
Higher-Order Logic	Towards the Verification of Higher-Order Logic Automated Reasoning
Higher-Order Rewriting	Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting
Higher-order term rewriting	Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
I
IMO	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
induction	Learning Conjecturing from Scratch
Innermost termination	Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
Instantiations	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Interactive and automated theorem proving	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
interactive theorem proving	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm Verified Path Indexing
interpolation	On Symbol Elimination and Uniform Interpolation in Theory Extensions
Invariant	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
invited talk	TBA TBA TBA
Isabelle/HOL	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
ITP	Interoperability of Proof systems with SC-TPTP (System Description)
K
Knuth-Bendix ordering	Term Ordering Diagrams
L
Lambda Calculus	The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting
Languages with binders	Equational Reasoning Modulo Commutativity in Languages with Binders
Lemmas	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
lexicographic path ordering	Term Ordering Diagrams
Local Search	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
Local Theories	Relatively Complete and Efficient Partial Quantifier Elimination
logic	TBA
Logically constrained term rewriting	Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs
M
machine learning	Learning Conjecturing from Scratch
Mathematical knowledge representation	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
MCSat	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
Metamath	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Modal Logic	From Modal Sequent Calculi to Modal Resolution
Model Checking	Infinite State Model Checking by Learning Transitive Relations A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Model Finding	Faithful Logic Embeddings in HOL – Deep and Shallow
N
Negative Free Logic	Cut Elimination for Negative Free Logics with Definite Descriptions
Non-classical logics	Faithful Logic Embeddings in HOL – Deep and Shallow
Non-Left-Linear Rewrite Rules	Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting
Non-Monotonic Logics	From Modal Sequent Calculi to Modal Resolution
non-redundant clause learning	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
Nonlinear Integer Arithmetic	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
NuPRL	TBA
O
Ontology	Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
ordered resolution	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
P
paramodulation	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
Partial Assignments	Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
Partial Quantifier Elimination	Relatively Complete and Efficient Partial Quantifier Elimination
pattern matching	Anti-pattern templates
polite theory combination	Being polite is not enough (and other limits of theory combination)
Polynomial Time Algorithm	Relatively Complete and Efficient Partial Quantifier Elimination
premise selection	Premise Selection with the Alternating-Path-Method
Program analysis	Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems
Program Verification	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Proof assistant systems	Faithful Logic Embeddings in HOL – Deep and Shallow
Proof calculus	A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Proof Checking	A Theorem Prover Based Approach for SAT-Based Model Checking Certification
Proof compression	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Proof Instability	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Proof structuring	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Proof Systems	Interoperability of Proof systems with SC-TPTP (System Description)
Proof Theoretic	Relatively Complete and Efficient Partial Quantifier Elimination
Proof Verification	Towards the Verification of Higher-Order Logic Automated Reasoning
Proof-producing decision procedure	Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
Q
Quantifier elimination	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
R
Real Algebra	More is Less: Adding Polynomials for Faster Explanations in NLSAT
Real arithmetic	SMT and Functional Equation Solving over the Reals: Challenges from the IMO
reasoning	TBA
Recurrence Analysis	Infinite State Model Checking by Learning Transitive Relations
redundancy	Partial Redundancy in Saturation
Resolution Calculi	From Modal Sequent Calculi to Modal Resolution
Rewriting	Analyzing Weighted Abstract Reduction Systems via Semirings
S
Safety	Infinite State Model Checking by Learning Transitive Relations A Theorem Prover Based Approach for SAT-Based Model Checking Certification
SAT encodings	Unfolding Boxes with Local Constraints
satisfiability	Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration Anti-pattern templates
satisfiability modulo theories	Being polite is not enough (and other limits of theory combination) Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
satisfiability modulo theory	Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
Saturation theorem proving	Computing Witnesses Using the SCAN Algorithm
saturation-based theorem proving	Partial Redundancy in Saturation Term Ordering Diagrams Efficient Neural Clause-Selection Reinforcement
SCAN algorithm	Computing Witnesses Using the SCAN Algorithm
SCL	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
Second-order quantifier elimination	Computing Witnesses Using the SCAN Algorithm
self-learning	Learning Conjecturing from Scratch
Semantic Difference	Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
Semantics	Analyzing Weighted Abstract Reduction Systems via Semirings
Semirings	Analyzing Weighted Abstract Reduction Systems via Semirings
Sequent Calculuis	From Modal Sequent Calculi to Modal Resolution
Sequent Calculus	Cut Elimination for Negative Free Logics with Definite Descriptions
shiny theory combination	Being polite is not enough (and other limits of theory combination)
Siemens	TBA
simplification ordering	Term Ordering Diagrams
Single Cell Construction	More is Less: Adding Polynomials for Faster Explanations in NLSAT
Sledgehammer	Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
SMT	Cazamariposas: Automated Instability Debugging in SMT-based Program Verification Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. On Symbol Elimination and Uniform Interpolation in Theory Extensions SMT and Functional Equation Solving over the Reals: Challenges from the IMO
SMT solvers	What's Decidable About Arrays With Sums?
SMT Solving	More is Less: Adding Polynomials for Faster Explanations in NLSAT
SNOMED CT	Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT
superposition calculus	Partial Redundancy in Saturation
symbol elimination	On Symbol Elimination and Uniform Interpolation in Theory Extensions
T
Tea Party	Welcome
term indexing	Verified Path Indexing
term rewriting	Lexicographic Combination of Reduction Pairs
Termination	The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting Lexicographic Combination of Reduction Pairs Analyzing Weighted Abstract Reduction Systems via Semirings
Theorem proving	A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
theorem proving	TBA
theory combination	Being polite is not enough (and other limits of theory combination)
TPTP	Review of the TPTP format for derivations Welcome
Transition Systems	Infinite State Model Checking by Learning Transitive Relations
U
unification	Equational Reasoning Modulo Commutativity in Languages with Binders Anti-pattern templates Verified Path Indexing
useful evaluation	A Fresh Inductive Approach to Useful Call-by-Value
V
Vampire	Efficient Neural Clause-Selection Reinforcement
Verification	Analyzing Weighted Abstract Reduction Systems via Semirings
verified algorithm	Verified Path Indexing
verified proofs	Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
W
Welcome	Welcome
Z
z3	Learning Conjecturing from Scratch

Disclaimer | Powered by EasyChair Smart Program