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

Days: Sunday, July 11th Monday, July 12th Tuesday, July 13th Wednesday, July 14th Thursday, July 15th Friday, July 16th

Sunday, July 11th

View this program: with abstractssession overviewtalk overview

10:00-10:30Break
12:00-12:30Break
14:00-14:30Break
Monday, July 12th

View this program: with abstractssession overviewtalk overview

08:00-09:00 Session 5: Invited Talk
Location: ZoomRoom 1
08:00
Taming Verification Conditions for Diagnosable Verification
09:00-10:00 Session 6: Theories (A)
Location: ZoomRoom 1
09:00
The ksmt calculus is a delta-complete decision procedure for non-linear constraints (abstract)
09:30
Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning (abstract)
10:00-10:30Break
10:30-12:30 Session 7: Logical Foundations
Location: ZoomRoom 1
10:30
Tableau-based decision procedure for non-Fregean logic of sentential identity (abstract)
11:00
Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (abstract)
11:30
Efficient Local Reductions to Basic Modal Logic (abstract)
12:00
Isabelle's Metalogic: Formalization and Proof Checker (abstract)
12:30-13:00Break
13:00-15:00 Session 8: Intuition and Induction
Location: ZoomRoom 1
13:00
Unifying Decidable Entailments in Separation Logic with Inductive Definitions (abstract)
13:30
Subformula Linking for Intuitionistic Logic and Type Theory (abstract)
14:00
Efficient SAT-based proof search in Intuitionistic Propositional Logic (abstract)
14:30
Proof Search and Certificates for Evidential Transactions (abstract)
Tuesday, July 13th

View this program: with abstractssession overviewtalk overview

08:00-10:00 Session 9: Theory in Practice
Location: ZoomRoom 1
08:00
Non-Clausal Redundancy Properties (abstract)
08:30
Multi-Dimensional Interpretation Methods for Termination of Term Rewriting (abstract)
09:00
Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (abstract)
09:30
Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes (abstract)
10:00-10:30Break
10:30-12:30 Session 10: Inference
Location: ZoomRoom 1
10:30
Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance (abstract)
11:00
A Unifying Splitting Framework (abstract)
11:30
Integer Induction in Saturation (abstract)
12:00
Superposition with First-Class Booleans and Inprocessing Clausification (abstract)
12:30-13:00Break
13:00-15:00 Session 11: Implementation
Location: ZoomRoom 1
13:00
Superposition for Full Higher-Order Logic (abstract)
13:30
Making Higher-Order Superposition Work (abstract)
14:00
Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver (abstract)
14:30
Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant (abstract)
15:00-15:30Break
15:30-16:30 Session 12: Invited Talk
Location: ZoomRoom 1
15:30
Computational Law: Automated Reasoning in the Legal Domain
Wednesday, July 14th

View this program: with abstractssession overviewtalk overview

08:00-09:00 Session 13: Invited Talk
Location: ZoomRoom 1
08:00
Non-well-founded Deduction for Induction and Coinduction
09:00-10:00 Session 14: Theories (B)
Location: ZoomRoom 1
09:00
Politeness and Stable Infiniteness: Stronger Together (abstract)
09:30
Equational Theorem Proving Modulo (abstract)
10:00-10:30Break
10:30-12:30 Session 15: Applications in Systems
Location: ZoomRoom 1
10:30
An Automated Approach to the Collatz Conjecture (abstract)
11:00
Verified interactive computation of definite integrals (abstract)
11:30
A Normative Supervisor for Reinforcement Learning Agents (System Description) (abstract)
11:45
Automatically Building Diagrams for Olympiad Geometry Problems (System Description) (abstract)
12:00
The Fusemate Logic Programming System (System Description) (abstract)
12:30-13:00Break
Thursday, July 15th

View this program: with abstractssession overviewtalk overview

08:00-10:00 Session 17: System Descriptions and Competition Reports
Location: ZoomRoom 1
08:00
Twee: an equational theorem prover (System Description) (abstract)
08:15
The Isabelle/Naproche Natural Language Proof Assistant (System Description) (abstract)
08:30
The Lean 4 Theorem Prover and Programming Language (System Description) (abstract)
08:45
Harpoon: Mechanizing Metatheory Interactively (System Description) (abstract)
09:00
CADE-28 ATP System Competition Results (abstract)
09:30
Termination and Complexity Competition Results (abstract)
10:00-10:30Break
10:30-12:00 Session 18: ATP+AI
Location: ZoomRoom 1
10:30
Confidences for Commonsense Reasoning (abstract)
11:00
Neural Precedence Recommender (abstract)
PRESENTER: Filip Bártek
11:30
New Techniques that Improve ENIGMA-style Clause Selection Guidance (abstract)
12:00-12:30Break
12:30-13:30 Session 19: Invited Talk
Location: ZoomRoom 1
12:30
Towards the Automatic Mathematician
13:30-14:00Break
Friday, July 16th

View this program: with abstractssession overviewtalk overview

10:00-10:30Break
12:00-12:30Break
14:00-14:30Break