| 2025 | A Fresh Inductive Approach to Useful Call-by-Value. Pablo Barenbaum, Delia Kesner, Mariana Milicich |
| 2025 | A Real-Analytic Approach to Differential-Algebraic Dynamic Logic. Jonathan Hellwig, André Platzer |
| 2025 | A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution. Martin Bromberger, Martin Desharnais, Christoph Weidenbach |
| 2025 | A Theorem Prover Based Approach for SAT-Based Model Checking Certification. Giulia Sindoni, Paolo Pasini, Gianpiero Cabodi, Paolo E. Camurati, Alberto Griggio, Marco Palena, Marco Roveri, Stefano Tonetta |
| 2025 | Anti-pattern Templates. Jan Otop |
| 2025 | Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings Clark W. Barrett, Uwe Waldmann |
| 2025 | Being Polite Is Not Enough (and Other Limits of Theory Combination). Guilherme Vicentin de Toledo, Benjamin Przybocki, Yoni Zohar |
| 2025 | Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. Enrico Lipparini, Thomas Hader, Ahmed Irfan, Stéphane Graham-Lengrand |
| 2025 | Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification. Yi Zhou, Amar Shah, Zhengyao Lin, Marijn Heule, Bryan Parno |
| 2025 | Choose Your Proofs: Commutativity and Symmetry for Smarter Reasoning. Azadeh Farzan |
| 2025 | Computing Ground Congruence Classes. Hendrik Leidinger, Christoph Weidenbach |
| 2025 | Computing Witnesses Using the SCAN Algorithm. Fabian Achammer, Stefan Hetzl, Renate A. Schmidt |
| 2025 | Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics. Franz Baader, Stefan Borgwardt, Filippo De Bortoli, Patrick Koopmann |
| 2025 | Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems. Salvador Lucas |
| 2025 | Cut Elimination for Negative Free Logics with Definite Descriptions. Andrzej Indrzejczak |
| 2025 | Efficient Neural Clause-Selection Reinforcement. Martin Suda |
| 2025 | Entailment vs. Verification for Partial-Assignment Satisfiability and Enumeration. Roberto Sebastiani |
| 2025 | Equational Reasoning Modulo Commutativity in Languages with Binders. Ali K. Caires-Santos, Maribel Fernández, Daniele Nantes-Sobrinho |
| 2025 | Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL. Lukas Bartl, Jasmin Blanchette, Tobias Nipkow |
| 2025 | Faithful Logic Embeddings in HOL - Deep and Shallow. Christoph Benzmüller |
| 2025 | From Modal Sequent Calculi to Modal Resolution. Dirk Pattinson, Cláudia Nalon, Sourabh Peruri |
| 2025 | Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories. Michael Rawson, Andrei Voronkov, Johannes Schoisswohl, Anja Petkovic Komel |
| 2025 | Infinite State Model Checking by Learning Transitive Relations. Florian Frohn, Jürgen Giesl |
| 2025 | Interoperability of Proof Systems with SC-TPTP. Simon Guilloud, Julie Cailler, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat, Viktor Kuncak |
| 2025 | Learning Conjecturing from Scratch. Thibault Gauthier, Josef Urban |
| 2025 | Lexicographic Combination of Reduction Pairs. Teppei Saito, Nao Hirokawa |
| 2025 | More is Less: Adding Polynomials for Faster Explanations in NLSAT. Valentin Promies, Jasper Nalbach, Erika Ábrahám, Paul Wagner |
| 2025 | On Symbol Elimination and Uniform Interpolation in Theory Extensions. Viorica Sofronie-Stokkermans |
| 2025 | Partial Redundancy in Saturation. Márton Hajdú, Laura Kovács, Andrei Voronkov |
| 2025 | Relatively Complete and Efficient Partial Quantifier Elimination. Estifanos Getachew, Arie Gurfinkel, Richard J. Trefler |
| 2025 | SMT and Functional Equation Solving over the Reals: Challenges from the IMO. Chad E. Brown, Karel Chvalovský, Mikolás Janota, Mirek Olsák, Stefan Ratschan |
| 2025 | Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm. Lukas Stevens, Rebecca Ghidini |
| 2025 | Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting. Thiago Felicissimo, Jean-Pierre Jouannaud |
| 2025 | Term Ordering Diagrams. Márton Hajdú, Robin Coutelier, Laura Kovács, Andrei Voronkov |
| 2025 | The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting. Johannes Niederhauser, Aart Middeldorp |
| 2025 | Unfolding Boxes with Local Constraints. Long Qian, Eric Wang, Bernardo Subercaseaux, Marijn J. H. Heule |
| 2025 | Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CT. Yizheng Zhao, Junyi Zhang, Renate A. Schmidt |
| 2025 | Verified Path Indexing. Mohamed Chaabani, Simon Robillard |
| 2025 | What's Decidable About Arrays With Sums? Roland Herrmann, Philipp Rümmer |