PROGRAM
Days: Wednesday, July 3rd Thursday, July 4th Friday, July 5th Saturday, July 6th
Wednesday, July 3rd
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 2: Invited Talk J. Avigad
Chair:
| 09:00 | Automated Reasoning for Mathematics |
| 10:00 | Certifying Phase Abstraction (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 3: Intuitionistic Logics
Chair:
| 11:00 | A Terminating Sequent Calculus for Intuitionistic Strong Löb Logic with the Subformula Property (abstract)  PRESENTER: Camillo Fiorentini |
| 11:30 | Skolemization for Intuitionistic Linear Logic (abstract) |
| 12:00 | Local Intuitionistic Modal Logics and Their Calculi (abstract) |
12:30-14:00Lunch Break
14:00-16:00 Session 4: Rewriting and Tool Presentations
Chair:
| 14:00 | A Dependency Pair Framework for Relative Termination of Term Rewriting (abstract) |
| 14:30 | Confluence of Logically Constrained Rewrite Systems Revisited (abstract) PRESENTER: Jonas Schöpf |
| 15:00 | The Naproche-ZF theorem prover (short paper/system description) (abstract) |
| 15:20 | Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper) (abstract) |
| 15:40 | A Higher-Order Vampire (abstract)  |
16:00-16:30Coffee Break
16:30-18:30 Session 5: Theorem Proving 1
Chair:
| 16:30 | Synthesis of Recursive Programs in Saturation (abstract) |
| 17:00 | Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic (abstract) |
| 17:30 | Lemma Discovery and Strategies for Automated Induction (abstract) |
| 18:00 | On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus (abstract) |
Thursday, July 4th
View this program: with abstractssession overviewtalk overview
08:30-10:00 Session 6: Invited Talk L. Kovacs
Chair:
| 08:30 | Induction in Saturation |
| 09:30 | The Benefits of Diligence (abstract) |
10:00-10:30Coffee Break
10:30-12:30 Session 8: IJCAR Best Paper & Modal Logics
Additional information: IJCAR PC co-chairs will also be present
Chair:
| 10:30 | Mechanised uniform interpolation for modal logics K, GL and iSL (abstract) |
| 11:00 | Non-Iterative Modal Resolution (abstract) |
| 11:30 | Model Construction for Modal Clauses (abstract) |
| 12:00 | A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems (abstract) |
12:30-14:00Lunch Break
14:00-16:00 Session 9: Satisfiability Solving
Chair:
| 14:00 | Certified MaxSAT Preprocessing (abstract) |
| 14:30 | Quantifier Shifting for Quantified Boolean Formulas Revisited (abstract) |
| 15:00 | SAT-based Learning of Computation Tree Logic (abstract) |
| 15:30 | Fast and Verified UNSAT Certificate Checking (abstract) |
16:00-16:30Coffee Break
16:30-17:00 Session 10: IJCAR Best Student Paper & Higher-Order Logic
Additional information: IJCAR PC co-chairs will also be present
Chair:
| 16:30 | Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (abstract) PRESENTER: Johannes Niederhauser |
17:00-18:15 Session 11: Awards Presentation (incl. Herbrand Award)
Additional information: The best paper awards will also be handed out (by the IJCAR PC co-chairs) in this session.
Chair:
19:30-22:30 Conference Dinner
Additional information: The dinner will also include a brief celebration of the 30th anniversary of the CASC competition.
Friday, July 5th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 12: Invited Talk G. Sutcliffe
Chair:
| 09:00 | Stepping Stones in the TPTP World |
| 10:00 | Equivalence Checking of Quantum Circuits by Model Counting (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 13: Decision Procedures
Chair:
| 11:00 | A Decision Method for First-Order Stream Logic (abstract) |
| 11:30 | What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment? (abstract) PRESENTER: Quentin Petitjean |
| 12:00 | Uniform Substitution for Differential Refinement Logic (abstract) |
12:30-14:00Lunch Break
14:00-16:00 Session 14A: Proof Theory and Calculi
Chair:
| 14:00 | Sequents vs hypersequents for Aqvist systems (abstract) |
| 14:30 | Sequent Systems on Undirected Graphs (abstract) |
| 15:00 | A proof theory of (omega) context-free languages, via non-wellfounded proofs (abstract) PRESENTER: Abhishek De |
| 15:30 | A cyclic proof system for Guarded Kleene Algebra with Tests (abstract) |
14:00-16:00 Session 14B: Theorem Proving 2
Chair:
| 14:00 | An Empirical Assessment of Progress in Automated Theorem Proving (abstract) |
| 14:30 | Reducibility Constraints in Superposition (abstract) |
| 15:00 | First-Order Automatic Literal Model Generation (abstract) |
| 15:30 | Regularization in Spider-style Strategy Discovery and Schedule Construction (abstract) PRESENTER: Filip Bártek |
16:00-16:30Coffee Break
16:30-17:30 Session 15: SAT and SMT Short Papers
Chair:
| 16:30 | MCSat-based Finite Field Reasoning in the Yices2 SMT Solver (abstract) |
| 16:50 | Verifying a Realistic Mutable Hash Table: Case Study (abstract) |
| 17:10 | Booleguru, the Propositional Polyglot (abstract) |
Saturday, July 6th
View this program: with abstractssession overviewtalk overview
08:30-10:00 Session 18: Unification
Chair:
| 08:30 | Solving Quantitative Equations (abstract) |
| 09:00 | Equational Anti-Unification over Absorption Theories (abstract) |
| 09:30 | Unification in the Description Logic ELHR+ without the Top Concept modulo Cycle-Restricted Ontologies (abstract) |
10:00-10:30Coffee Break
10:30-12:30 Session 19: Satisfiability Modulo Theories
Additional information: After this session, the conference will be closed by the IJCAR co-organisers and PC co-chairs.
Chair:
| 10:30 | Model Completeness for Rational Trees (abstract) PRESENTER: Silvio Ghilardi |
| 11:00 | Satisfiability Modulo Exponential Integer Arithmetic (abstract) |
| 11:30 | A Formal Model to Prove Instantiation Termination for E-matching-based Axiomatisations (abstract) |
| 12:00 | Generalized Optimization Modulo Theories (abstract) |