CADE-28: THE 28TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
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
Location: ZoomRoom 1
08:00
Formal Reasoning about Decentralized Financial Applications (abstract)
09:00-10:00 Session 13: 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 14: 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 15: 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)
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.

Location: ZoomLobby
15:30-16:00 Session 16: Topical ZoomRoom Teasers
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?
15:50
Step into the Darkside - Non-classical Logics
PRESENTER: Cláudia Nalon
15:55
Law, Morality, Religion, and ATP
Tuesday, July 13th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:00-10:00 Session 19: 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 21: 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 22: 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 23: Invited Talk
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
Location: ZoomRoom 1
08:00
Non-well-founded Deduction for Induction and Coinduction (abstract)
09:00-10:00 Session 26: 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 27: 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
13:00-16:10 Session 28: Awards
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
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
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
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