PROGRAM
Days: Monday, July 28th Tuesday, July 29th Wednesday, July 30th Thursday, July 31st Friday, August 1st Saturday, August 2nd
Monday, July 28th
View this program: with abstractssession overviewtalk overview
08:45-09:00 Session 1: Welcome
Location: A0.06
09:00-10:00 Session 2: CADE Invited Talk
| 09:00 | Choose Your Proofs: Commutativity and Symmetry for Smarter Reasoning |
10:00-10:30 Session 3: SMT I
| 10:00 | Being polite is not enough (and other limits of theory combination) (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 4: SMT II
| 11:00 | On Symbol Elimination and Uniform Interpolation in Theory Extensions (abstract) |
| 11:30 | What's Decidable About Arrays With Sums? (abstract) |
| 12:00 | Cazamariposas: Automated Instability Debugging in SMT-based Program Verification (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 5: SMT III
| 14:00 | Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. (abstract) |
| 14:30 | More is Less: Adding Polynomials for Faster Explanations in NLSAT (abstract) |
| 15:00 | Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories (abstract) |
| 15:15 | SMT and Functional Equation Solving over the Reals: Challenges from the IMO (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 6: Rewriting
| 16:00 | Lexicographic Combination of Reduction Pairs (abstract) |
| 16:30 | Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems (abstract) |
| 17:00 | The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (abstract) |
| 17:30 | Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting (abstract) |
Tuesday, July 29th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 7: CADE Invited Talk
| 09:00 | Taming Infinity for Verification in First-Order Logic |
10:00-10:30 Session 8: Short Talks
| 10:00 | Interoperability of Proof systems with SC-TPTP (System Description) (abstract) |
| 10:15 | Verified Path Indexing (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 9: Formalizations in Isabelle/HOL
| 11:00 | Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm (abstract) |
| 11:30 | Faithful Logic Embeddings in HOL – Deep and Shallow (abstract) |
| 12:00 | A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 10: Calculi
| 14:00 | Cut Elimination for Negative Free Logics with Definite Descriptions (abstract) |
| 14:30 | From Modal Sequent Calculi to Modal Resolution (abstract) |
| 15:00 | A Fresh Inductive Approach to Useful Call-by-Value (abstract) |
15:30-16:00Coffee Break
16:00-17:00 Session 11: Machine Learning for Automated Deduction
| 16:00 | Efficient Neural Clause-Selection Reinforcement (abstract) |
| 16:30 | Learning Conjecturing from Scratch (abstract) |
Wednesday, July 30th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 13: Model Checking and Quantifier Elimination
| 09:00 | A Theorem Prover Based Approach for SAT-Based Model Checking Certification (abstract) |
| 09:30 | Infinite State Model Checking by Learning Transitive Relations (abstract) |
| 10:00 | Relatively Complete and Efficient Partial Quantifier Elimination (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 14: Saturation
| 11:00 | Computing Witnesses Using the SCAN Algorithm (abstract) |
| 11:30 | Partial Redundancy in Saturation (abstract) |
| 12:00 | Term Ordering Diagrams (abstract) |
12:30-13:30Lunch Break
Thursday, July 31st
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 15: CADE Invited Talk
| 09:00 | A Decade of Lean: Advancing Proof Automation for Mathematics and Software Verification |
10:00-10:30 Session 16: Paramodulation
| 10:00 | Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 17: Equational Reasoning
| 11:00 | Computing Ground Congruence Classes (abstract) |
| 11:30 | Anti-pattern templates (abstract) |
| 12:00 | Equational Reasoning Modulo Commutativity in Languages with Binders (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 18: Non-Classical Logics
| 14:00 | Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT (abstract) |
| 14:30 | Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (abstract) |
| 15:00 | A Real-Analytic Approach to Differential-Algebraic Dynamic Logic (abstract) |
15:30-16:00Coffee Break
16:00-17:00 Session 19: SAT
| 16:00 | Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration (abstract) |
| 16:30 | Unfolding Boxes with Local Constraints (abstract) |
Friday, August 1st
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 21B: Deduktionstreffen (1)
Chair:
| 09:00 | TBA |
| 10:00 | Premise Selection with the Alternating-Path-Method (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 22B: Deduktionstreffen (2)
Chair:
| 11:00 | TBA |
| 12:00 | Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures (abstract) |
12:30-14:00Noon Break
14:00-15:30 Session 23B: Deduktionstreffen (3)
Chair:
| 14:00 | TBA |
| 15:00 | Towards the Verification of Higher-Order Logic Automated Reasoning (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 24B: Deduktionstreffen (4)
Chair:
| 16:00 | Analyzing Weighted Abstract Reduction Systems via Semirings (abstract) |
| 16:30 | Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs (abstract) PRESENTER: Carsten Fuhs |
Saturday, August 2nd
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 25D: TPTPTP (1)
Chair:
| 09:00 | Welcome |
| 09:10 | Review of the TPTP format for derivations |
10:30-11:00Coffee Break
12:30-14:00Noon Break
15:30-16:00Coffee Break