| 2024 | Generalized Optimization Modulo Theories. | Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli |
| 2024 | An Empirical Assessment of Progress in Automated Theorem Proving. | Geoff Sutcliffe, Christian B. Suttner, Lars Kotthoff, C. Raymond Perrault, Zain Khalid |
| 2024 | Stepping Stones in the TPTP World. | Geoff Sutcliffe |
| 2024 | Confluence of Logically Constrained Rewrite Systems Revisited. | Jonas Schpf, Fabian Mitterwallner, Aart Middeldorp |
| 2024 | A Decision Method for First-Order Stream Logic. | Harald Ruess |
| 2024 | A Cyclic Proof System for Guarded Kleene Algebra with Tests. | Jan Rooduijn, Dexter Kozen, Alexandra Silva |
| 2024 | Uniform Substitution for Differential Refinement Logic. | Enguerrand Prebet, Andr Platzer |
| 2024 | SAT-Based Learning of Computation Tree Logic. | Adrien Pommellet, Daniel Stan, Simon Scatton |
| 2024 | Non-iterative Modal Resolution Calculi. | Dirk Pattinson, Cludia Nalon |
| 2024 | Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic. | Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk |
| 2024 | Equivalence Checking of Quantum Circuits by Model Counting. | Jingyi Mei, Tim Coopmans, Marcello M. Bonsangue, Alfons Laarman |
| 2024 | The Naproche-ZF Theorem Prover (Short Paper). | Adrian De Lon |
| 2024 | Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper) - (Short Paper). | Nils Lommen, lanore Meyer, Jrgen Giesl |
| 2024 | Fast and Verified UNSAT Certificate Checking. | Peter Lammich |
| 2024 | Induction in Saturation. | Laura Kovcs, Petra Hozzov, Mrton Hajd, Andrei Voronkov |
| 2024 | A Dependency Pair Framework for Relative Termination of Term Rewriting. | Jan-Christoph Kassing, Grigory Vartanyan, Jrgen Giesl |
| 2024 | Certified MaxSAT Preprocessing. | Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Jrvisalo, Magnus O. Myreen, Jakob Nordstrm |
| 2024 | Model Construction for Modal Clauses. | Ullrich Hustadt, Fabio Papacchini, Cludia Nalon, Clare Dixon |
| 2024 | Synthesis of Recursive Programs in Saturation. | Petra Hozzov, Daneshvar Amrollahi, Mrton Hajd, Laura Kovcs, Andrei Voronkov, Eva Maria Wagner |
| 2024 | Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic. | Jan Heuer, Christoph Wernhard |
| 2024 | Booleguru, the Propositional Polyglot (Short Paper). | Maximilian Heisinger, Simone Heisinger, Martina Seidl |
| 2024 | Quantifier Shifting for Quantified Boolean Formulas Revisited. | Simone Heisinger, Maximilian Heisinger, Adrian Rebola-Pardo, Martina Seidl |
| 2024 | Reducibility Constraints in Superposition. | Mrton Hajd, Laura Kovcs, Michael Rawson, Andrei Voronkov |
| 2024 | MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). | Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stphane Graham-Lengrand, Laura Kovcs |
| 2024 | Model Completeness for Rational Trees. | Silvio Ghilardi, Lia M. Poidomani |