IJCAR PROGRAM
Days: Monday, August 8th Tuesday, August 9th Wednesday, August 10th
Monday, August 8th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 94D: Invited Talk and Cooperating Reasoners
Chair:
| 09:00 | From the Universality of Mathematical Truth to the Interoperability of Proof Systems (Invited Talk)   |
| 10:00 | Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description) (abstract) PRESENTER: Gereon Kremer |
10:30-11:00Coffee Break
11:00-12:30 Session 96D: Effective Superposition and Orderings
Chair:
| 11:00 | SCL(EQ): SCL for First-Order Logic with Equality (abstract) PRESENTER: Christoph Weidenbach |
| 11:20 | Ground joinability and connectedness in the superposition calculus (abstract) PRESENTER: André Duarte |
| 11:40 | Term Ordering for Non-Reachability of (Conditional) Rewriting (abstract) |
| 12:00 | An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (abstract)  PRESENTER: Lorenz Leutgeb |
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, IJCAR, ITP).
14:00-15:30 Session 97D: Knowledge Representation and Justification
Chair:
| 14:00 | Actions over Core-closed Knowledge Bases (abstract) PRESENTER: Claudia Cauli |
| 14:20 | GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (abstract) PRESENTER: Tanel Tammet |
| 14:35 | Local Reductions for the Modal Cube (abstract) PRESENTER: Cláudia Nalon |
| 14:55 | Evonne: Interactive Proof Visualization for Description Logics (System Description) (abstract) PRESENTER: Patrick Koopmann |
| 15:10 | Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications (abstract) PRESENTER: Hui Yang |
15:30-16:00Coffee Break
16:00-17:30 Session 98D: Preprocessing and Simplification
Chair:
| 16:00 | SAT-based Proof Search in Intermediate Propositional Logics (abstract) PRESENTER: Camillo Fiorentini |
| 16:20 | Preprocessing of Propagation Redundant Clauses (abstract) PRESENTER: Joseph Reeves |
| 16:40 | Clause Redundancy and Preprocessing in Maximum Satisfiability (abstract) PRESENTER: Jeremias Berg |
| 17:00 | Formula Simplification via Invariance Detection by Algebraically Indexed Types (ONLINE) (abstract) PRESENTER: Tomohiro Fujita |
18:30-20:30 Walking tour (at Haifa)
pickup at 18:00 from the Technion (Tour at Haifa, no food will be provided)
Tuesday, August 9th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 100D: Choices, Substitutions and Formalizations
Chair:
| 09:00 | Sequent Calculi for Choice Logics (abstract) PRESENTER: Michael Bernreiter |
| 09:20 | Lash 1.0 (System Description) (abstract) PRESENTER: Cezary Kaliszyk |
| 09:35 | Goéland : A Concurrent Tableau-Based Theorem Prover (System Description) (abstract)  PRESENTER: Julie Cailler |
| 09:50 | Synthetic tableaux: minimal tableau search heuristics (abstract) PRESENTER: Dorota Leszczyńska-Jasion |
| 10:10 | Binary codes that do not preserve primitivity (abstract) PRESENTER: Štěpán Holub |
10:30-11:00Coffee Break
11:00-12:30 Session 102D: Proof Systems and Recursion
Chair:
| 11:00 | Finite two-dimensional proof systems for non-finitely axiomatizable logics (abstract) PRESENTER: Vitor Rodrigues Greati |
| 11:20 | Le\'sniewski's Ontology -- Proof-Theoretic Characterization (abstract) |
| 11:40 | Cyclic Proofs, Hypersequents, and Transitive Closure Logic (abstract) PRESENTER: Marianna Girlando |
| 12:00 | Rensets and Renaming-Based Recursion for Syntax and Bindings (abstract) |
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, IJCAR, ITP).
14:00-15:30 Session 104D: Proof Search and Generalizations
Chair:
| 14:00 | Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (abstract) PRESENTER: Chaitanya Mangla |
| 14:20 | Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description) (abstract) |
| 14:35 | Semantic Relevance (abstract) PRESENTER: Christoph Weidenbach |
| 14:55 | Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (abstract) PRESENTER: Santiago Escobar |
| 15:10 | A framework for approximate generalization in quantitative theories (ONLINE) (abstract) PRESENTER: Temur Kutsia |
16:00-16:30Coffee Break
16:30-17:30 Session 108: Plenary
Chair:
Location: Churchill Auditorium
| 16:30 | SMT-based Verification of Distributed Network Control Planes (abstract) |
Wednesday, August 10th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 110D: System Evolution and Termination
Chair:
| 09:00 | CTL* model checking for data-aware dynamic systems with arithmetic (abstract) PRESENTER: Sarah Winkler |
| 09:20 | Implicit Definitions with Differential Equations for KeYmaera X (System Description) (abstract) PRESENTER: Yong Kiam Tan |
| 09:35 | On eventual non-negativity and positivity for the weighted sum of powers of matrices (abstract) PRESENTER: Supratik Chakraborty |
| 09:55 | Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (abstract) PRESENTER: Florian Frohn |
| 10:10 | Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (abstract) PRESENTER: Nils Lommen |
10:30-11:00Coffee Break
11:00-12:30 Session 112D: Decidable Logics and Models
Chair:
| 11:00 | Connection-minimal Abduction in EL via translation to FOL (abstract) PRESENTER: Sophie Tourret |
| 11:20 | Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (abstract) PRESENTER: Lucas Bueri |
| 11:40 | Reasoning About Vectors using an SMT Theory of Sequences (abstract) PRESENTER: Clark Barrett |
| 12:00 | Flexible Proof Production in an Industrial-Strength SMT Solver (abstract) PRESENTER: Haniel Barbosa |
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, IJCAR, ITP).
14:00-15:30 Session 115C: Invited Talk and Optimized Reasoning
Chair:
| 14:00 | Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts PRESENTER: Elvira Albert |
| 15:00 | Guiding an Automated Theorem Prover with Neural Rewriting (abstract) PRESENTER: Jelle Piepenbrock |
15:30-16:00Coffee Break
16:00-17:00 Session 116C: Modalities and Decidability
Chair:
| 16:00 | Non-associative, non-commutative multi-modal linear logic (abstract) PRESENTER: Stepan Kuznetsov |
| 16:20 | Paraconsistent Gödel modal logic (abstract) PRESENTER: Daniil Kozhemiachenko |
| 16:40 | Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (abstract) PRESENTER: Yoni Zohar |