| 2023 | A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). Mathias Fleury, Peter Lammich |
| 2023 | A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification). Yu-Fang Chen, Philipp Rümmer, Wei-Lun Tsai |
| 2023 | A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus. Andrzej Indrzejczak, Yaroslav I. Petrukhin |
| 2023 | An Experimental Pipeline for Automated Reasoning in Natural Language (Short Paper). Tanel Tammet, Priit Järv, Martin Verrev, Dirk Draheim |
| 2023 | An Isabelle/HOL Formalization of the SCL(FOL) Calculus. Martin Bromberger, Martin Desharnais, Christoph Weidenbach |
| 2023 | Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings Brigitte Pientka, Cesare Tinelli |
| 2023 | Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic. Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon |
| 2023 | COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description). Oliver Görlitz, Daniel Hausmann, Merlin Humml, Dirk Pattinson, Simon Prucker, Lutz Schröder |
| 2023 | Certified Core-Guided MaxSAT Solving. Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Dieter Vandesande |
| 2023 | Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT. Elisabeth Henkel, Jochen Hoenicke, Tanja Schindler |
| 2023 | Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett |
| 2023 | Confluence Criteria for Logically Constrained Rewrite Systems. Jonas Schöpf, Aart Middeldorp |
| 2023 | Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. Bernard Boigelot, Pascal Fontaine, Baptiste Vergain |
| 2023 | Formal Reasoning About Influence in Natural Sciences Experiments. Florian Bruse, Martin Lange, Sören Möller |
| 2023 | Incremental Rewriting Modulo SMT. Gerald Whitters, Vivek Nigam, Carolyn L. Talcott |
| 2023 | Iscalc: An Interactive Symbolic Computation Framework (System Description). Bohua Zhan, Yuheng Fan, Weiqiang Xiong, Runqing Xu |
| 2023 | Left-Linear Completion with AC Axioms. Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp |
| 2023 | On Incremental Pre-processing for SMT. Nikolaj S. Bjørner, Katalin Fazekas |
| 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 | Program Synthesis in Saturation. Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov |
| 2023 | Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs. Jan-Christoph Kassing, Jürgen Giesl |
| 2023 | Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper). Florian Frohn, Jürgen Giesl |
| 2023 | Proving Termination of C Programs with Lists. Jera Hensel, Jürgen Giesl |
| 2023 | QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier |
| 2023 | Reasoning About Regular Properties: A Comparative Study. Tomás Fiedor, Lukás Holík, Martin Hruska, Adam Rogalewicz, Juraj Síc, Pavol Vargovcík |
| 2023 | SAT-Based Subsumption Resolution. Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath |
| 2023 | SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. Martin Bromberger, Chaahat Jain, Christoph Weidenbach |
| 2023 | Superposition with Delayed Unification. Ahmed Bhayat, Johannes Schoisswohl, Michael Rawson |
| 2023 | Theorem Proving in Dependently-Typed Higher-Order Logic. Colin Rothgang, Florian Rabe, Christoph Benzmüller |
| 2023 | Towards Fast Nominal Anti-unification of Letrec-Expressions. Manfred Schmidt-Schauß, Daniele Nantes-Sobrinho |
| 2023 | Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory. Lukas Stevens |
| 2023 | Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs. Marvin Brieger, Stefan Mitsch, André Platzer |
| 2023 | Verification of NP-Hardness Reduction Functions for Exact Lattice Problems. Katharina Kreuzer, Tobias Nipkow |
| 2023 | Verified Given Clause Procedures. Jasmin Blanchette, Qi Qiu, Sophie Tourret |