CADE-28 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 overviewside by side with other conferences
10:00-10:30Break
12:00-12:30Break
14:00-14:30Break
Monday, July 12th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:00-09:00 Session 12: Invited Talk
Chair:
Location: ZoomRoom 1
| 08:00 | Formal Reasoning about Decentralized Financial Applications (abstract) |
09:00-10:00 Session 13: Theories (A)
Chair:
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 14: Logical Foundations
Chair:
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 15: Intuition and Induction
Chair:
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) |
15:00-15:30Break
15:30-16:30 Reception
The CADE-28 (online) reception, a time to meet and interact with friends and foes in the automated reasoning community. It's open bar (BYO), tasty hors d'oeuvres(BYO), and live entertainment ... there will be five "topical sessions", each led by experts in the topical areas. To start it off the experts will give 5 minute teasers for their topics. Then for the second 30 minutes there will be five breakout ZoomRooms in which the experts will lead and listen to discussion of their topics. People can join and leave the topical rooms, to enjoy some interesting interactions. Remember that the ChatRooms are available if you want head off for a private discussion.
Chair:
Location: ZoomLobby
15:30-16:00 Session 16: Topical ZoomRoom Teasers
Chair:
Location: ZoomRoom 1
| 15:30 | Reception Opening |
| 15:35 | Newbie's Meeting Place PRESENTER: Ruzica Piskac |
| 15:40 | 17 Ways to make an ATP System Fast PRESENTER: Stephan Schulz |
| 15:45 | How can Anyone Trust a Theorem Prover? PRESENTER: Anders Schlichtkrull |
| 15:50 | Step into the Darkside - Non-classical Logics PRESENTER: Cláudia Nalon |
| 15:55 | Law, Morality, Religion, and ATP PRESENTER: Christoph Benzmüller |
16:00-16:30 Session 17B: Topical ZoomRoom: 17 Ways to make an ATP System Fast
Chair:
Location: ZoomRoom 3
16:00-16:30 Session 17C: Topical ZoomRoom: How can Anyone Trust a Theorem Prover?
Chair:
Location: ZoomRoom 4
16:00-16:30 Session 17D: Topical ZoomRoom: Step into the Darkside - Non-classical Logics
Chair:
Location: ZoomRoom 5
16:00-16:30 Session 17E: Topical ZoomRoom: Morality, Religion, Law, and ATP
Chair:
Location: ZoomRoom 6
Tuesday, July 13th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:00-10:00 Session 19: Theory in Practice
Chair:
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 21: Inference
Chair:
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 22: Implementation
Chair:
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 23: Invited Talk
Chair:
Location: ZoomRoom 1
| 15:30 | Computational Law: Automated Reasoning in the Legal Domain |
Wednesday, July 14th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:00-09:00 Session 25: Invited Talk
Chair:
Location: ZoomRoom 1
| 08:00 | Non-well-founded Deduction for Induction and Coinduction (abstract) |
09:00-10:00 Session 26: Theories (B)
Chair:
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 27: Applications in Systems
Chair:
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
13:00-16:10 Session 28: Awards
Chair:
Location: ZoomRoom 1
| 13:00 | Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem |
| 14:15 | 2020 Herbrand Award |
| 14:25 | Unification, Combination, Description Logics, and All That (abstract) |
| 15:05 | Break |
| 15:15 | 2021 Herbrand Award |
| 15:25 | Isabelle: Growing and Applying a Proof Assistant |
Thursday, July 15th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:00-10:00 Session 30: System Descriptions and Competition Reports
Chair:
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 | The CADE-28 ATP System Competition (CASC-28) Results (abstract) |
| 09:30 | Termination and Complexity Competition Results (abstract) |
10:00-10:30Break
10:30-12:00 Session 31: ATP+AI
Chair:
Location: ZoomRoom 1
| 10:30 | Confidences for Commonsense Reasoning (abstract) |
| 11:00 | Neural Precedence Recommender (abstract) PRESENTER: Filip Bártek |
| 11:30 | Improving ENIGMA-Style Clause Selection While Learning From History (abstract) |
12:00-12:30Break
12:30-13:30 Session 32: Invited Talk
Chair:
Location: ZoomRoom 1
| 12:30 | Towards the Automatic Mathematician (abstract) |
13:30-14:00Break
Friday, July 16th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
10:00-10:30Break
12:00-12:30Break
14:00-14:30Break