Program

11:00	Viorica Sofronie-Stokkermans On Symbol Elimination and Uniform Interpolation in Theory Extensions (abstract)
11:30	Roland Herrmann and Philipp Rümmer What's Decidable About Arrays With Sums? (abstract)
12:00	Yi Zhou, Amar Shah, Zhengyao Lin, Marijn Heule and Bryan Parno Cazamariposas: Automated Instability Debugging in SMT-based Program Verification (abstract)

12:30-14:00Lunch Break

14:00-15:30 Session 6: SMT III

Chair:

Viorica Sofronie-Stokkermans

Location: A0.06

14:00	Enrico Lipparini, Thomas Hader, Ahmed Irfan and Stéphane Graham-Lengrand Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. (abstract)
14:30	Valentin Promies, Jasper Nalbach, Erika Abraham and Paul Wagner More is Less: Adding Polynomials for Faster Explanations in NLSAT (abstract)
15:00	Andrei Voronkov, Michael Rawson, Anja Petković Komel and Johannes Schoisswohl Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories (abstract)
15:15	Chad Brown, Karel Chvalovský, Mikoláš Janota, Miroslav Olšák and Stefan Ratschan SMT and Functional Equation Solving over the Reals: Challenges from the IMO (abstract)

15:30-16:00Coffee Break

16:00-18:00 Session 7: Rewriting

Chair:

Carsten Fuhs

Location: A0.06

16:00	Teppei Saito and Nao Hirokawa Lexicographic Combination of Reduction Pairs (abstract)
16:30	Salvador Lucas Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems (abstract)
17:00	Johannes Niederhauser and Aart Middeldorp The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (abstract) PRESENTER: Johannes Niederhauser
17:30	Thiago Felicissimo and Jean-Pierre Jouannaud Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting (abstract)

18:00-20:00 Welcome Reception

Location: Roof Terrace

Tuesday, July 29th

View this program: with abstracts session overview talk overview

09:00-10:00 Session 8: CADE Invited Talk

Chair:

Uwe Waldmann

Location: A0.06

09:00

Sharon Shoham

Taming Infinity for Verification in First-Order Logic

10:00-10:30 Session 9: Short Talks

Chair:

Pascal Fontaine

Location: A0.06

10:00	Simon Guilloud, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat, Viktor Kuncak and Julie Cailler Interoperability of Proof systems with SC-TPTP (System Description) (abstract)
10:15	Mohamed Chaabani and Simon Robillard Verified Path Indexing (abstract)

10:30-11:00Coffee Break

11:00-12:30 Session 10: Formalizations in Isabelle/HOL

Chair:

Mathias Fleury

Location: A0.06

11:00	Lukas Stevens and Rebecca Ghidini Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm (abstract)
11:30	Christoph Benzmüller Faithful Logic Embeddings in HOL – Deep and Shallow (abstract)
12:00	Martin Bromberger, Martin Desharnais and Christoph Weidenbach A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution (abstract)

12:30-14:00Lunch Break

14:00-15:30 Session 11: Calculi

Location: A0.06

14:00	Andrzej Indrzejczak Cut Elimination for Negative Free Logics with Definite Descriptions (abstract)
14:30	Dirk Pattinson, Cláudia Nalon and Sourabh Peruri From Modal Sequent Calculi to Modal Resolution (abstract)
15:00	Pablo Barenbaum, Delia Kesner and Mariana Milicich A Fresh Inductive Approach to Useful Call-by-Value (abstract)

15:30-16:00Coffee Break

16:00-17:00 Session 12: Machine Learning for Automated Deduction

Chair:

Mikoláš Janota

Location: A0.06

16:00	Martin Suda Efficient Neural Clause-Selection Reinforcement (abstract)
16:30	Thibault Gauthier and Josef Urban Learning Conjecturing from Scratch (abstract)

17:00-18:30 Session 13: Awards

Chairs:

Uwe Waldmann and Clark Barrett

Location: A0.06

Wednesday, July 30th

View this program: with abstracts session overview talk overview

09:00-10:30 Session 14A: Model Checking and Quantifier Elimination

Chair:

Ali Uncu

Location: A0.06

09:00	Gianpiero Cabodi, Paolo Enrico Camurati, Alberto Griggio, Marco Palena, Paolo Pasini, Marco Roveri, Giulia Sindoni and Stefano Tonetta A Theorem Prover Based Approach for SAT-Based Model Checking Certification (abstract)
09:30	Florian Frohn and Jürgen Giesl Infinite State Model Checking by Learning Transitive Relations (abstract)
10:00	Estifanos Getachew, Arie Gurfinkel and Richard Trefler Relatively Complete and Efficient Partial Quantifier Elimination (abstract) PRESENTER: Estifanos Getachew

09:00-16:00 Session 14B: CASC

Location: A0.07

10:30-11:00Coffee Break

11:00-12:30 Session 15: Saturation

Chair:

Martin Suda

Location: A0.06

11:00	Fabian Achammer, Stefan Hetzl and Renate A. Schmidt Computing Witnesses Using the SCAN Algorithm (abstract)
11:30	Marton Hajdu, Laura Kovács and Andrei Voronkov Partial Redundancy in Saturation (abstract)
12:00	Marton Hajdu, Robin Coutelier, Laura Kovács and Andrei Voronkov Term Ordering Diagrams (abstract)

12:30-13:30Lunch Break

13:30-18:00 Conference Excursion

18:00-22:00 Conference Dinner

Thursday, July 31st

View this program: with abstracts session overview talk overview

09:00-10:00 Session 16: CADE Invited Talk

Chair:

Clark Barrett

Location: A0.06

09:00

Leonardo de Moura

A Decade of Lean: Advancing Proof Automation for Mathematics and Software Verification

10:00-10:30 Session 17: Paramodulation

Location: A0.06

10:00

Lukas Bartl, Jasmin Blanchette and Tobias Nipkow

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL (abstract)

10:30-11:00Coffee Break

11:00-12:30 Session 18: Equational Reasoning

Chair:

Nao Hirokawa

Location: A0.06

11:00	Hendrik Leidinger and Christoph Weidenbach Computing Ground Congruence Classes (abstract)
11:30	Jan Otop Anti-pattern templates (abstract)
12:00	Ali Khan Caires Ribeiro Santos, Maribel Fernandez and Daniele Nantes Sobrinho Equational Reasoning Modulo Commutativity in Languages with Binders (abstract)

12:30-14:00Lunch Break

14:00-15:30 Session 19: Non-Classical Logics

Chair:

Christoph Weidenbach

Location: A0.06

14:00	Yizheng Zhao and Renate A. Schmidt Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT (abstract)
14:30	Franz Baader, Stefan Borgwardt, Filippo De Bortoli and Patrick Koopmann Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (abstract) PRESENTER: Filippo De Bortoli
15:00	Jonathan Hellwig and André Platzer A Real-Analytic Approach to Differential-Algebraic Dynamic Logic (abstract)

15:30-16:00Coffee Break

16:00-17:00 Session 20: SAT

Chair:

Mathias Fleury

Location: A0.06

16:00	Roberto Sebastiani Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration (abstract)
16:30	Long Qian, Eric Wang, Bernardo Subercaseaux and Marijn Heule Unfolding Boxes with Local Constraints (abstract)

17:00-18:00 Session 21: Business Meeting

Location: A0.06

Friday, August 1st

View this program: with abstracts session overview talk overview

09:00-10:30 Session 22A: Deduktionstreffen (1)

Chair:

Uwe Waldmann

09:00	Ullrich Hustadt TBA
10:00	Jannis Gehring and Stephan Schulz Premise Selection with the Alternating-Path-Method (abstract)

09:00-10:30 Session 22B: Weidenbach60 (1)

Location: A0.07

09:00	Christoph Weidenbach TBA
10:00	Sophie Tourret Conflict-based Literal Model Generation (abstract)

09:00-09:30 Session 22C: Automated Deduction in Geometry - Welcome

Welcome ADG25

Chair:

Pedro Quaresma

09:30-10:30 Session 23: Automated Deduction in Geometry (1st session)

Chair:

Pedro Quaresma

09:30	András Kerekes and Zoltán Kovács Towards automatic detection of geometric difficulty of geometry problems (abstract)
10:00	Michael Katzenberger and Jürgen Richter-Gebert Manifold-based Proving Methods in Projective Geometry (abstract)

10:30-11:00Coffee Break

11:00-12:00 Session 24A: Automated Deduction in Geometry (2)

Chair:

Pedro Quaresma

11:00	Predrag Janicic and Julien Narboux Geometry Machine Revisited (abstract)
11:30	Gábor Gévay, Benedek Kovács and Zoltán Kovács Is a regular polygon determined by its diagonals? (abstract)

11:00-12:30 Session 24B: Deduktionstreffen (2)

Chair:

Florian Rabe

11:00	Christoph Kreitz TBA
12:00	Christoph Wernhard and Zsolt Zombori Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures (abstract)

11:00-12:30 Session 24C: Weidenbach60 (2)

Location: A0.07

11:00	Stephan Merz Invariant Synthesis: Decidable Fragments to the Rescue (abstract)
11:30	Renate A. Schmidt and Hongkai Yin Applying SCAN to Basic Path Logic and the Ordered Fragment (Extended Abstract) (abstract)
12:00	David Plaisted and Stephan Schulz Planning with Equality (abstract)

12:30-14:00Noon Break

14:00-15:30 Session 25A: Automated Deduction in Geometry (3)

Chair:

Zoltán Kovács

14:00	Álvaro Pereira-Albert, Tomas Recio and M. Pilar Velez Computing loci with GeoGebra Discovery: some issues and suggestions (abstract)
14:30	Shivam Sharma and John Keyser Inference Maximizing Point Configurations for Parsimonious Algorithms (abstract)

14:00-15:30 Session 25B: Deduktionstreffen (3)

Chair:

Kai Sauerwald

14:00	Thomas Hubauer TBA
15:00	Melanie Taprogge Towards the Verification of Higher-Order Logic Automated Reasoning (abstract)

14:00-15:30 Session 25C: Weidenbach60 (3)

Location: A0.07

14:00	Valentin Promies and Erika Abraham Solving Non-Linear Optimization with the Cylindrical Algebraic Covering Method (abstract)
14:30	Guilherme Toledo, Benjamin Przybocki and Yoni Zohar Polite theory combination, an overview (abstract)
15:00	Yasmine Briefs and Mathias Fleury From Building Blocks to Real SAT Solvers (abstract)

15:30-16:00Coffee Break

16:00-17:30 Session 26A: Automated Deduction in Geometry (4)

Chair:

Zoltán Kovács

16:00	Vesna Marinkovic, Tijana Sukilovic and Filip Maric Different Types of Locus Dependencies in Solving Geometry Construction Problems (abstract)
16:30	Pedro Quaresma and Pierluigi Graziani Towards a Structural Analysis of Interesting Geometric Theorems: Analysis of a Survey (abstract)
17:00	Thierry Dana-Picard Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration (abstract)

16:00-18:00 Session 26B: Deduktionstreffen (4)

Chair:

Florian Rabe

16:00	Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl and Joost-Pieter Katoen Analyzing Weighted Abstract Reduction Systems via Semirings (abstract)
16:30	Carsten Fuhs, Liye Guo and Cynthia Kop Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs (abstract) PRESENTER: Carsten Fuhs

16:00-18:00 Session 26C: Weidenbach60 (4)

Location: A0.07

16:00	Geoff Sutcliffe, Sean Holden and Mantas Baksys The TPTP Format for Tableaux Proofs (abstract)
16:30	Massin Guerdi A Lambda-Superposition Tactic for Isabelle/HOL (abstract)
17:00	Jørgen Villadsen, Simon Tobias Lund and Anders Schlichtkrull Formalizing Axiomatics for First-Order Logic (abstract)

Saturday, August 2nd

View this program: with abstracts session overview talk overview

09:00-10:30 Session 27A: Automated Deduction in Geometry (5)

Chair:

Julien Narboux

09:00	Vesna Marinković Automating Geometry Construction Problems
10:00	Yoan Géran and Pierre Boutry First-Order Simplification of GeoCoq using Dedukti (abstract) PRESENTER: Pierre Boutry

09:00-10:30 Session 27B: Satisfiability Checking and Symbolic Computation (1)

09:00-10:00 Session 27C: Theorem Proving Components for Educational Software (joint session with ADG)

Invited Talk by Vesna Marinkovic

Chair:

Julien Narboux

09:00-10:30 Session 27D: TPTPTP (1)

Chair:

Geoff Sutcliffe

09:00	Geoff Sutcliffe Welcome
09:10	Geoff Sutcliffe Review of the TPTP format for derivations
09:30	Geoff Sutcliffe Proof Verification with GDV and GDV-LP
10:00	Melanie Taprogge Leo-III and LambdaPi

10:30-11:00Coffee Break

11:00-12:00 Session 28A: Automated Deduction in Geometry (6)

Chair:

Julien Narboux

11:00	Alexandre Jean, Pierre Boutry and Nicolas Magaud An Automated Approach towards Constructivizing the GeoCoq Library (abstract) PRESENTER: Alexandre Jean
11:30	Prunelle Colin and Pierre Boutry On the Coq/Rocq Mechanization of Beeson's "On the Notion of Equal Figures in Euclid" (abstract)

11:00-12:30 Session 28B: Satisfiability Checking and Symbolic Computation (2)

11:00-12:00 Session 28C: Theorem Proving Components for Educational Software (2)

Chair:

Pedro Quaresma

11:00	Jelle Wemmenhove, Nick Hoofd, Alexander Schüler-Meyer and Jim Portegies Reinforcing students’ proof structure with Waterproof: an analysis (abstract)
11:30	Simone Heisinger, Katharina Blaimschein and Martina Seidl Evaluating LLMs on Formal Models Coursework (abstract)

11:00-12:30 Session 28D: TPTPTP (2)

Chair:

Geoff Sutcliffe

11:00	Anja Petkovic Komel Vampire and Dedukti
11:30	Michael Rawson Higher-order Verification of Skolemization Steps
12:00	Martin Suda Equisatisfiable Inferences

12:30-14:00Noon Break

14:00-15:30 Session 29A: Automated Deduction in Geometry (7)

Chair:

Pierre Boutry

14:00	Pedro Quaresma, Predrag Janicic, Julien Narboux, Zoltán Kovács, Anna Petiurenko, Filip Marić and Nuno Baeta ADG-Lib Initiative (abstract)
14:30	Pedro Quaresma and Nuno Baeta A Generator of Geometry Deductive Database Method Provers (abstract)

14:00-15:30 Session 29B: Satisfiability Checking and Symbolic Computation (3)

14:00-15:00 Session 29C: Theorem Proving Components for Educational Software (3)

14:00	Romain Sidhoum and Simon Robillard Teaching Automated Deduction: an Implementation-BasedApproach with Maude (abstract)
14:30	Jørgen Villadsen Teaching Axiomatic Systems and Metatheory in Isabelle (abstract)

14:00-15:30 Session 29D: TPTPTP (3)

Chair:

Michael Rawson

14:00	Sean Holden The TPTP Format for Clausal Connection Tableau Proofs
14:30	Alex Steen The TPTP Format for Interpretations
15:00	Julie Callier The ProoVer Competition at IJCAR 2026

15:00-15:30 Session 30: Theorem Proving Components for Educational Software - Business Meeting

Chair:

Jørgen Villadsen

15:30-16:00Coffee Break

16:00-17:00 Session 31A: Automated Deduction in Geometry (8)

Chair:

Pierre Boutry

16:00	Roland Coghetto IsaGeoCoq, a port of GeoCoq with Isabelle/HOL (abstract)
16:30	Zoltán Kovács Proving theorems on regular polygons by elimination --- the elementary way (abstract)

16:00-18:00 Session 31B: Satisfiability Checking and Symbolic Computation (4)

16:00-18:00 Session 31C: TPTPTP (4)

Chair:

Michael Rawson

16:00	David Fuenmayor StarExec-ARC
16:30	Wine And Cheese Action Planning == Wish List

17:00-17:30 Session 32: Automated Deduction in Geometry - Business Meeting

Chairs:

Pedro Quaresma and Julien Narboux