Accepted Papers

The list of accepted papers is also available with abstracts.

Fabian Achammer, Stefan Hetzl and Renate A. Schmidt. Computing Witnesses Using the SCAN Algorithm (details)
Tanbir Ahmed, Lamina Zaman and Curtis Bright. [FP] Symbolic Sets for Proving Bounds on Rado Numbers (details)
Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl and Joost-Pieter Katoen. Analyzing Weighted Abstract Reduction Systems via Semirings (details)
Franz Baader, Stefan Borgwardt, Filippo De Bortoli and Patrick Koopmann. Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (details)
Pablo Barenbaum, Delia Kesner and Mariana Milicich. A Fresh Inductive Approach to Useful Call-by-Value (details)
Lukas Bartl, Jasmin Blanchette and Tobias Nipkow. Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL (details)
Christoph Benzmüller. Faithful Logic Embeddings in HOL – A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level (details)
Jasmin Blanchette, Mathias Fleury, Martin Suda and Sophie Tourret. First-Order Reasoning, Below and Beyond: Workshop in Honor of Christoph Weidenbach’s 60th Birthday (details)
Yasmine Briefs and Mathias Fleury. From Building Blocks to Real SAT Solvers (details)
Martin Bromberger, Martin Desharnais and Christoph Weidenbach. A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution (details)
Chad Brown, Karel Chvalovský, Mikoláš Janota, Miroslav Olšák and Stefan Ratschan. SMT and Functional Equation Solving over the Reals: Challenges from the IMO (details)
Christopher W. Brown. Presentation Only: Semantics of Division for Polynomial Solvers (details)
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 (details)
Ali Khan Caires Ribeiro Santos, Maribel Fernandez and Daniele Nantes Sobrinho. Equational Reasoning Modulo Commutativity in Languages with Binders (details)
Mohamed Chaabani and Simon Robillard. Verified Path Indexing (details)
Roland Coghetto. IsaGeoCoq, a port of GeoCoq with Isabelle/HOL (details)
Prunelle Colin and Pierre Boutry. On the Coq/Rocq Mechanization of Beeson's "On the Notion of Equal Figures in Euclid" (details)
Thierry Dana-Picard. Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration (details)
Thiago Felicissimo and Jean-Pierre Jouannaud. Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting (details)
Florian Frohn and Jürgen Giesl. Infinite State Model Checking by Learning Transitive Relations (details)
Carsten Fuhs, Liye Guo and Cynthia Kop. Proving Call-by-value Termination of Constrained Higher-order Rewriting by Dependency Pairs (details)
Thibault Gauthier and Josef Urban. Learning Conjecturing from Scratch (details)
Jannis Gehring and Stephan Schulz. Premise Selection with the Alternating-Path-Method (details)
Estifanos Getachew, Arie Gurfinkel and Richard Trefler. Relatively Complete and Efficient Partial Quantifier Elimination (details)
Massin Guerdi. A Lambda-Superposition Tactic for Isabelle/HOL (details)
Simon Guilloud, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat, Viktor Kuncak and Julie Cailler. Interoperability of Proof systems with SC-TPTP (System Description) (details)
Yoan Géran and Pierre Boutry. First-Order Simplification of GeoCoq using Dedukti (details)
Gábor Gévay, Benedek Kovács and Zoltán Kovács. Is a regular polygon determined by its diagonals? (details)
Thomas Hader, Ahmed Irfan and Stéphane Graham-Lengrand. PO: Decision Heuristics in MCSat (details)
Marton Hajdu, Robin Coutelier, Laura Kovács and Andrei Voronkov. Term Ordering Diagrams (details)
Marton Hajdu, Laura Kovács and Andrei Voronkov. Partial Redundancy in Saturation (details)
Simone Heisinger, Katharina Blaimschein and Martina Seidl. Evaluating LLMs on Formal Models Coursework (details)
Jonathan Hellwig and André Platzer. A Real-Analytic Approach to Differential-Algebraic Dynamic Logic (details)
Roland Herrmann and Philipp Rümmer. What's Decidable About Arrays With Sums? (details)
Andrzej Indrzejczak. Cut Elimination for Negative Free Logics with Definite Descriptions (details)
Predrag Janicic and Julien Narboux. Geometry Machine Revisited (details)
Alexandre Jean, Pierre Boutry and Nicolas Magaud. An Automated Approach towards Constructivizing the GeoCoq Library (details)
Michael Katzenberger and Jürgen Richter-Gebert. Manifold-based Proving Methods in Projective Geometry (details)
Daniela Kaufmann and James Davenport. 10th SC-Square Workshop (details)
Daniela Kaufmann and Clemens Hofstadler. EA Recycling Algebraic Proof Certificates (details)
András Kerekes and Zoltán Kovács. Towards automatic detection of geometric difficulty of geometry problems (details)
Laura Kovács and Michael Rawson. Vampire 2025: The 9th Vampire Workshop (details)
Zoltán Kovács and Pedro Quaresma. Automated Deduction in Geometry (ADG’25) (details)
Zoltán Kovács. Proving theorems on regular polygons by elimination --- the elementary way (details)
Hendrik Leidinger and Christoph Weidenbach. Computing Ground Congruence Classes (details)
Enrico Lipparini, Thomas Hader, Ahmed Irfan and Stéphane Graham-Lengrand. Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. (details)
Salvador Lucas. Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems (details)
Alessio Mansutti. PO Integer Linear-Exponential Programming (details)
Vesna Marinkovic, Tijana Sukilovic and Filip Maric. Different Types of Locus Dependencies in Solving Geometry Construction Problems (details)
Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark Barrett and Cesare Tinelli. PO Formalization of a Proof Calculus for Incremental Linearization for NTA and NRA Satisfiability (details)
Stephan Merz. Invariant Synthesis: Decidable Fragments to the Rescue (details)
Jasper Nalbach, Lucas Michel, Erika Abraham, Christopher Brown, James H. Davenport, Matthew England, Pierre Mathonet and Naïm Zenaïdi. FP Projective Delineability for Single Cell Construction (details)
Jasper Nalbach and Erika Ábrahám. FP A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination (details)
Julien Narboux, Walther Neuper, Jørgen Villadsen and Pedro Quaresma. Theorem Proving Components for Educational Software (ThEdu'25) Proposal for a Workshop at CADE 2025 (details)
Johannes Niederhauser and Aart Middeldorp. The Computability Path Ordering for Beta-Eta-Normal Higher-Order Rewriting (details)
Jan Otop. Anti-pattern templates (details)
Dirk Pattinson, Cláudia Nalon and Sourabh Peruri. From Modal Sequent Calculi to Modal Resolution (details)
Álvaro Pereira-Albert, Tomas Recio and M. Pilar Velez. Computing loci with GeoGebra Discovery: some issues and suggestions (details)
Valentin Promies, Jasper Nalbach, Erika Abraham and Paul Wagner. More is Less: Adding Polynomials for Faster Explanations in NLSAT (details)
Long Qian, Eric Wang, Bernardo Subercaseaux and Marijn Heule. Unfolding Boxes with Local Constraints (details)
Pedro Quaresma and Nuno Baeta. A Generator of Geometry Deductive Database Method Provers (details)
Pedro Quaresma and Pierluigi Graziani. Towards a Structural Analysis of Interesting Geometric Theorems: Analysis of a Survey (details)
Pedro Quaresma, Predrag Janicic, Julien Narboux, Zoltán Kovács, Anna Petiurenko, Filip Marić and Nuno Baeta. ADG-Lib Initiative (details)
Florian Rabe, Uwe Waldmann, Özgür Lütfü Özcep and Kai Sauerwald. Deduktionstreffen (details)
Teppei Saito and Nao Hirokawa. Lexicographic Combination of Reduction Pairs (details)
Renate A. Schmidt and Hongkai Yin. Applying SCAN to Basic Path Logic and the Ordered Fragment (Extended Abstract) (details)
Roberto Sebastiani. Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration (details)
Shivam Sharma and John Keyser. Inference Maximizing Point Configurations for Parsimonious Algorithms (details)
Romain Sidhoum and Simon Robillard. Teaching Automated Deduction: an Implementation-BasedApproach with Maude (details)
Viorica Sofronie-Stokkermans. On Symbol Elimination and Uniform Interpolation in Theory Extensions (details)
Lukas Stevens and Rebecca Ghidini. Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm (details)
Martin Suda. Efficient Neural Clause-Selection Reinforcement (details)
Geoff Sutcliffe. The CADE-30 ATP System Competition (CASC-30) (details)
Geoff Sutcliffe. The TPTP Tea Party (TPTPTP) (details)
Melanie Taprogge. Towards the Verification of Higher-Order Logic Automated Reasoning (details)
Guilherme Toledo, Benjamin Przybocki and Yoni Zohar. Being polite is not enough (and other limits of theory combination) (details)
Guilherme Toledo, Benjamin Przybocki and Yoni Zohar. Polite theory combination, an overview (details)
Sophie Tourret. Conflict-based Literal Model Generation (details)
Jørgen Villadsen, Simon Tobias Lund and Anders Schlichtkrull. Formalizing Axiomatics for First-Order Logic (details)
Jørgen Villadsen. Teaching Axiomatic Systems and Metatheory in Isabelle (details)
Andrei Voronkov, Michael Rawson, Anja Petković Komel and Johannes Schoisswohl. Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories (details)
Jelle Wemmenhove, Nick Hoofd, Alexander Schüler-Meyer and Jim Portegies. Reinforcing students’ proof structure with Waterproof: an analysis (details)
Christoph Wernhard and Zsolt Zombori. Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures (details)
Yizheng Zhao and Renate A. Schmidt. Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT (details)
Yi Zhou, Amar Shah, Zhengyao Lin, Marijn Heule and Bryan Parno. Cazamariposas: Automated Instability Debugging in SMT-based Program Verification (details)