| 2024 | A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations. | Rui Ge, Ronald Garcia, Alexander J. Summers |
| 2024 | Certifying Phase Abstraction. | Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko |
| 2024 | Satisfiability Modulo Exponential Integer Arithmetic. | Florian Frohn, Jrgen Giesl |
| 2024 | A Terminating Sequent Calculus for Intuitionistic Strong Lb Logic with the Subformula Property. | Camillo Fiorentini, Mauro Ferrari |
| 2024 | Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL. | Hugo Fre, Iris van der Giessen, Sam van Gool, Ian Shillito |
| 2024 | Lemma Discovery and Strategies for Automated Induction. | Slrn Halla Einarsdttir, Mrton Hajd, Moa Johansson, Nicholas Smallbone, Martin Suda |
| 2024 | Solving Quantitative Equations. | Georg Ehling, Temur Kutsia |
| 2024 | A Logic for Repair and State Recovery in Byzantine Fault-Tolerant Multi-agent Systems. | Hans van Ditmarsch, Krisztina Fruzsa, Roman Kuznets, Ulrich Schmid |
| 2024 | A Proof Theory of (mega-)Context-Free Languages, via Non-wellfounded Proofs. | Anupam Das, Abhishek De |
| 2024 | Sequents vs Hypersequents for qvist Systems. | Agata Ciabattoni, Matteo Tesi |
| 2024 | Verifying a Realistic Mutable Hash Table - Case Study (Short Paper). | Samuel Chassot, Viktor Kuncak |
| 2024 | Skolemisation for Intuitionistic Linear Logic. | Alessandro Bruni, Eike Ritter, Carsten Schrmann |
| 2024 | First-Order Automatic Literal Model Generation. | Martin Bromberger, Florent Krasnopol, Sibylle Mhle, Christoph Weidenbach |
| 2024 | What Is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment? | Tanguy Bozec, Nicolas Peltier, Quentin Petitjean, Mihaela Sighireanu |
| 2024 | A Higher-Order Vampire (Short Paper). | Ahmed Bhayat, Martin Suda |
| 2024 | Regularization in Spider-Style Strategy Discovery and Schedule Construction. | Filip Brtek, Karel Chvalovsk, Martin Suda |
| 2024 | Local Intuitionistic Modal Logics and Their Calculi. | Philippe Balbiani, Han Gao, igdem Gencer, Nicola Olivetti |
| 2024 | Unification in the Description Logic | Franz Baader, Oliver Fernndez Gil |
| 2024 | Equational Anti-unification over Absorption Theories. | Mauricio Ayala-Rincn, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia |
| 2024 | Automated Reasoning for Mathematics. | Jeremy Avigad |
| 2024 | The Benefits of Diligence. | Victor Arrial, Giulio Guerrieri, Delia Kesner |
| 2024 | Sequent Systems on Undirected Graphs. | Matteo Acclavio |