| 2021 | A Normative Supervisor for Reinforcement Learning Agents. Emery A. Neufeld, Ezio Bartocci, Agata Ciabattoni, Guido Governatori |
| 2021 | A Unifying Splitting Framework. Gabriel Ebner, Jasmin Blanchette, Sophie Tourret |
| 2021 | An Automated Approach to the Collatz Conjecture. Emre Yolcu, Scott Aaronson, Marijn J. H. Heule |
| 2021 | Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings André Platzer, Geoff Sutcliffe |
| 2021 | Automatically Building Diagrams for Olympiad Geometry Problems. Ryan Krueger, Jesse Michael Han, Daniel Selsam |
| 2021 | Computing Optimal Repairs of Quantified ABoxes w.r.t. Static Franz Baader, Patrick Koopmann, Francesco Kriegel, Adrian Nuradiansyah |
| 2021 | Confidences for Commonsense Reasoning. Tanel Tammet, Dirk Draheim, Priit Järv |
| 2021 | Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. Randal E. Bryant, Marijn J. H. Heule |
| 2021 | Efficient Local Reductions to Basic Modal Logic. Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon |
| 2021 | Efficient SAT-based Proof Search in Intuitionistic Propositional Logic. Camillo Fiorentini |
| 2021 | Equational Theorem Proving Modulo. Dohan Kim, Christopher Lynch |
| 2021 | Finding Good Proofs for Description Logic Entailments using Recursive Quality Measures. Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, Alisa Kovtunova |
| 2021 | Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. Fajar Haifani, Sophie Tourret, Christoph Weidenbach |
| 2021 | Harpoon: Mechanizing Metatheory Interactively - (System Description). Jacob Errington, Junyoung Jang, Brigitte Pientka |
| 2021 | Improving ENIGMA-style Clause Selection while Learning From History. Martin Suda |
| 2021 | Integer Induction in Saturation. Petra Hozzová, Laura Kovács, Andrei Voronkov |
| 2021 | Isabelle's Metalogic: Formalization and Proof Checker. Tobias Nipkow, Simon Roßkopf |
| 2021 | Learning from Łukasiewicz and Meredith: Investigations into Proof Structures. Christoph Wernhard, Wolfgang Bibel |
| 2021 | Making Higher-Order Superposition Work. Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret |
| 2021 | Multi-Dimensional Interpretations for Termination of Term Rewriting. Akihisa Yamada |
| 2021 | Neural Precedence Recommender. Filip Bártek, Martin Suda |
| 2021 | Non-clausal Redundancy Properties. Lee A. Barnett, Armin Biere |
| 2021 | Non-well-founded Deduction for Induction and Coinduction. Liron Cohen |
| 2021 | Politeness and Stable Infiniteness: Stronger Together. Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | Proof Search and Certificates for Evidential Transactions. Vivek Nigam, Giselle Reis, Samar Rahmouni, Harald Ruess |
| 2021 | Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais |
| 2021 | Subformula Linking for Intuitionistic Logic with Application to Type Theory. Kaustuv Chaudhuri |
| 2021 | Superposition for Full Higher-order Logic. Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic |
| 2021 | Superposition with First-class Booleans and Inprocessing Clausification. Visa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirovic |
| 2021 | Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity. Joanna Golinska-Pilarek, Taneli Huuskonen, Michal Zawidzki |
| 2021 | The Fusemate Logic Programming System. Peter Baumgartner |
| 2021 | The Isabelle/Naproche Natural Language Proof Assistant. Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Makarius Wenzel |
| 2021 | The Lean 4 Theorem Prover and Programming Language. Leonardo de Moura, Sebastian Ullrich |
| 2021 | The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints. Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller |
| 2021 | Towards the Automatic Mathematician. Markus N. Rabe, Christian Szegedy |
| 2021 | Twee: An Equational Theorem Prover. Nicholas Smallbone |
| 2021 | Unifying Decidable Entailments in Separation Logic with Inductive Definitions. Mnacho Echenim, Radu Iosif, Nicolas Peltier |
| 2021 | Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning. Alessandro Cimatti, Alberto Griggio, Gianluca Redondi |
| 2021 | Verified Interactive Computation of Definite Integrals. Runqing Xu, Liming Li, Bohua Zhan |