| 2025 | Learning Conjecturing from Scratch. | Thibault Gauthier, Josef Urban |
| 2025 | Infinite State Model Checking by Learning Transitive Relations. | Florian Frohn, Jrgen Giesl |
| 2025 | Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting. | Thiago Felicissimo, Jean-Pierre Jouannaud |
| 2025 | Choose Your Proofs: Commutativity and Symmetry for Smarter Reasoning. | Azadeh Farzan |
| 2025 | Verified Path Indexing. | Mohamed Chaabani, Simon Robillard |
| 2025 | Equational Reasoning Modulo Commutativity in Languages with Binders. | Ali K. Caires-Santos, Maribel Fernndez, Daniele Nantes-Sobrinho |
| 2025 | SMT and Functional Equation Solving over the Reals: Challenges from the IMO. | Chad E. Brown, Karel Chvalovsk, Mikols Janota, Mirek Olsk, Stefan Ratschan |
| 2025 | A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution. | Martin Bromberger, Martin Desharnais, Christoph Weidenbach |
| 2025 | Faithful Logic Embeddings in HOL - Deep and Shallow. | Christoph Benzmller |
| 2025 | Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL. | Lukas Bartl, Jasmin Blanchette, Tobias Nipkow |
| 2025 | A Fresh Inductive Approach to Useful Call-by-Value. | Pablo Barenbaum, Delia Kesner, Mariana Milicich |
| 2025 | Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics. | Franz Baader, Stefan Borgwardt, Filippo De Bortoli, Patrick Koopmann |
| 2025 | Computing Witnesses Using the SCAN Algorithm. | Fabian Achammer, Stefan Hetzl, Renate A. Schmidt |
| 2023 | Iscalc: An Interactive Symbolic Computation Framework (System Description). | Bohua Zhan, Yuheng Fan, Weiqiang Xiong, Runqing Xu |
| 2023 | Incremental Rewriting Modulo SMT. | Gerald Whitters, Vivek Nigam, Carolyn L. Talcott |
| 2023 | Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. | Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett |
| 2023 | An Experimental Pipeline for Automated Reasoning in Natural Language (Short Paper). | Tanel Tammet, Priit Jrv, Martin Verrev, Dirk Draheim |
| 2023 | Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory. | Lukas Stevens |
| 2023 | Confluence Criteria for Logically Constrained Rewrite Systems. | Jonas Schpf, Aart Middeldorp |
| 2023 | Towards Fast Nominal Anti-unification of Letrec-Expressions. | Manfred Schmidt-Schau, Daniele Nantes-Sobrinho |
| 2023 | Theorem Proving in Dependently-Typed Higher-Order Logic. | Colin Rothgang, Florian Rabe, Christoph Benzmller |
| 2023 | On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics | Dennis Peuter, Viorica Sofronie-Stokkermans, Sebastian Thunert |
| 2023 | Left-Linear Completion with AC Axioms. | Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp |
| 2023 | Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic. | Cludia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon |
| 2023 | Verification of NP-Hardness Reduction Functions for Exact Lattice Problems. | Katharina Kreuzer, Tobias Nipkow |