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

A
Aaronson, Scott	An Automated Approach to the Collatz Conjecture
Alrabbaa, Christian	Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
B
Baader, Franz	Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes Unification, Combination, Description Logics, and All That
Barnett, Lee	Non-Clausal Redundancy Properties
Barrett, Clark	Politeness and Stable Infiniteness: Stronger Together
Bartocci, Ezio	A Normative Supervisor for Reinforcement Learning Agents (System Description)
Baumgartner, Peter	The Fusemate Logic Programming System (System Description)
Bentkamp, Alexander	Superposition with First-Class Booleans and Inprocessing Clausification Superposition for Full Higher-Order Logic Making Higher-Order Superposition Work
Benzmüller, Christoph	Law, Morality, Religion, and ATP
Bibel, Wolfgang	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Biere, Armin	Non-Clausal Redundancy Properties
Bjørner, Nikolaj	Newbie's Meeting Place
Blanchette, Jasmin	A Unifying Splitting Framework Superposition for Full Higher-Order Logic Making Higher-Order Superposition Work
Bonacina, Maria Paola	Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
Borgwardt, Stefan	Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
Brauße, Franz	The ksmt calculus is a delta-complete decision procedure for non-linear constraints
Bryant, Randal	Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver
Bártek, Filip	Neural Precedence Recommender
C
Chaudhuri, Kaustuv	Subformula Linking for Intuitionistic Logic and Type Theory
Ciabattoni, Agata	A Normative Supervisor for Reinforcement Learning Agents (System Description)
Cimatti, Alessandro	Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
Cohen, Liron	Non-well-founded Deduction for Induction and Coinduction
Cruanes, Simon	Making Higher-Order Superposition Work
D
De Lon, Adrian	The Isabelle/Naproche Natural Language Proof Assistant (System Description)
de Moura, Leonardo	The Lean 4 Theorem Prover and Programming Language (System Description)
Desharnais, Martin	Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Dixon, Clare	Efficient Local Reductions to Basic Modal Logic
Draheim, Dirk	Confidences for Commonsense Reasoning
E
Ebner, Gabriel	A Unifying Splitting Framework How can Anyone Trust a Theorem Prover?
Echenim, Mnacho	Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Errington, Jacob	Harpoon: Mechanizing Metatheory Interactively (System Description)
F
Fiorentini, Camillo	Efficient SAT-based proof search in Intuitionistic Propositional Logic
Fleury, Mathias	Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Fontaine, Pascal	Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
Fuenmayor, David	Law, Morality, Religion, and ATP
G
Giesl, Jürgen	2021 Herbrand Award
Golińska-Pilarek, Joanna	Tableau-based decision procedure for non-Fregean logic of sentential identity
Governatori, Guido	A Normative Supervisor for Reinforcement Learning Agents (System Description) Computational Law: Automated Reasoning in the Legal Domain
Griggio, Alberto	Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
H
Haifani, Fajar	Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
Heule, Marijn	An Automated Approach to the Collatz Conjecture Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver
Hozzová, Petra	Integer Induction in Saturation
Hustadt, Ullrich	Efficient Local Reductions to Basic Modal Logic
Huuskonen, Taneli	Tableau-based decision procedure for non-Fregean logic of sentential identity
I
Iosif, Radu	Unifying Decidable Entailments in Separation Logic with Inductive Definitions
J
Jang, Junyoung	Harpoon: Mechanizing Metatheory Interactively (System Description)
Järv, Priit	Confidences for Commonsense Reasoning
K
Kim, Dohan	Equational Theorem Proving Modulo
Koepke, Peter	The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Koopmann, Patrick	Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes
Korovin, Konstantin	The ksmt calculus is a delta-complete decision procedure for non-linear constraints
Korovina, Margarita	The ksmt calculus is a delta-complete decision procedure for non-linear constraints
Kovtunova, Alisa	Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
Kovács, Laura	Integer Induction in Saturation Newbie's Meeting Place
Kriegel, Francesco	Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes
Krueger, Ryan	Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
L
Li, Liming	Verified interactive computation of definite integrals
Lorenzen, Anton	The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Lynch, Christopher	Equational Theorem Proving Modulo
M
Marti, Adrian	The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Michael Han, Jesse	Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Müller, Norbert Th.	The ksmt calculus is a delta-complete decision procedure for non-linear constraints
N
Nalon, Cláudia	Efficient Local Reductions to Basic Modal Logic Step into the Darkside - Non-classical Logics
Neufeld, Emery	A Normative Supervisor for Reinforcement Learning Agents (System Description)
Nigam, Vivek	Proof Search and Certificates for Evidential Transactions
Nipkow, Tobias	Isabelle's Metalogic: Formalization and Proof Checker
Nipkow, Tobias	Isabelle: Growing and Applying a Proof Assistant
Nummelin, Visa	Superposition with First-Class Booleans and Inprocessing Clausification Making Higher-Order Superposition Work
Nuradiansyah, Adrian	Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes
P
Papacchini, Fabio	Efficient Local Reductions to Basic Modal Logic
Peltier, Nicolas	Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Pientka, Brigitte	Harpoon: Mechanizing Metatheory Interactively (System Description)
Piskac, Ruzica	Newbie's Meeting Place
Platzer, André	Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
R
Rabe, Markus N.	Towards the Automatic Mathematician
Rahmouni, Samar	Proof Search and Certificates for Evidential Transactions
Redondi, Gianluca	Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
Reis, Giselle	Proof Search and Certificates for Evidential Transactions
Reynolds, Andrew	Politeness and Stable Infiniteness: Stronger Together
Ringeissen, Christophe	Politeness and Stable Infiniteness: Stronger Together
Roßkopf, Simon	Isabelle's Metalogic: Formalization and Proof Checker
Ruess, Harald	Proof Search and Certificates for Evidential Transactions
S
Sagiv, Mooly	Formal Reasoning about Decentralized Financial Applications
Schlichtkrull, Anders	How can Anyone Trust a Theorem Prover?
Schulz, Stephan	17 Ways to make an ATP System Fast
Schurr, Hans-Jörg	Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Schütz, Marcel	The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Selsam, Daniel	Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Sheng, Ying	Politeness and Stable Infiniteness: Stronger Together
Smallbone, Nicholas	Twee: an equational theorem prover (System Description)
Steen, Alexander	Step into the Darkside - Non-classical Logics
Suda, Martin	Neural Precedence Recommender Improving ENIGMA-Style Clause Selection While Learning From History
Sutcliffe, Geoff	The CADE-28 ATP System Competition (CASC-28) Results Reception Opening
Szegedy, Christian	Towards the Automatic Mathematician
T
Tammet, Tanel	Confidences for Commonsense Reasoning
Tinelli, Cesare	Politeness and Stable Infiniteness: Stronger Together
Tourret, Sophie	Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance A Unifying Splitting Framework Superposition with First-Class Booleans and Inprocessing Clausification Superposition for Full Higher-Order Logic Making Higher-Order Superposition Work
U
Ullrich, Sebastian	The Lean 4 Theorem Prover and Programming Language (System Description)
V
Voronkov, Andrei	Integer Induction in Saturation 2020 Herbrand Award
Vukmirović, Petar	Superposition with First-Class Booleans and Inprocessing Clausification Superposition for Full Higher-Order Logic Making Higher-Order Superposition Work 17 Ways to make an ATP System Fast
W
Weidenbach, Christoph	Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance Break
Wenzel, Makarius	The Isabelle/Naproche Natural Language Proof Assistant (System Description)
Wernhard, Christoph	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
X
Xu, Runqing	Verified interactive computation of definite integrals
Y
Yamada, Akihisa	Multi-Dimensional Interpretation Methods for Termination of Term Rewriting Termination and Complexity Competition Results
Yolcu, Emre	An Automated Approach to the Collatz Conjecture
Z
Zawidzki, Michał	Tableau-based decision procedure for non-Fregean logic of sentential identity
Zhan, Bohua	Verified interactive computation of definite integrals
Zohar, Yoni	Politeness and Stable Infiniteness: Stronger Together

Disclaimer | Powered by EasyChair Smart Program