| 2021 | Making Higher-Order Superposition Work. | Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret |
| 2021 | Confidences for Commonsense Reasoning. | Tanel Tammet, Dirk Draheim, Priit Jrv |
| 2021 | Twee: An Equational Theorem Prover. | Nicholas Smallbone |
| 2021 | Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. | Hans-Jrg Schurr, Mathias Fleury, Martin Desharnais |
| 2021 | Towards the Automatic Mathematician. | Markus N. Rabe, Christian Szegedy |
| 2021 | Efficient Local Reductions to Basic Modal Logic. | Fabio Papacchini, Cludia Nalon, Ullrich Hustadt, Clare Dixon |
| 2021 | Superposition with First-class Booleans and Inprocessing Clausification. | Visa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirovic |
| 2021 | Isabelle's Metalogic: Formalization and Proof Checker. | Tobias Nipkow, Simon Rokopf |
| 2021 | Proof Search and Certificates for Evidential Transactions. | Vivek Nigam, Giselle Reis, Samar Rahmouni, Harald Ruess |
| 2021 | A Normative Supervisor for Reinforcement Learning Agents. | Emery A. Neufeld, Ezio Bartocci, Agata Ciabattoni, Guido Governatori |
| 2021 | The Lean 4 Theorem Prover and Programming Language. | Leonardo de Moura, Sebastian Ullrich |
| 2021 | The Isabelle/Naproche Natural Language Proof Assistant. | Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schtz, Makarius Wenzel |
| 2021 | Automatically Building Diagrams for Olympiad Geometry Problems. | Ryan Krueger, Jesse Michael Han, Daniel Selsam |
| 2021 | Integer Induction in Saturation. | Petra Hozzov, Laura Kovcs, Andrei Voronkov |
| 2021 | Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. | Fajar Haifani, Sophie Tourret, Christoph Weidenbach |
| 2021 | Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity. | Joanna Golinska-Pilarek, Taneli Huuskonen, Michal Zawidzki |
| 2021 | Efficient SAT-based Proof Search in Intuitionistic Propositional Logic. | Camillo Fiorentini |
| 2021 | Harpoon: Mechanizing Metatheory Interactively - (System Description). | Jacob Errington, Junyoung Jang, Brigitte Pientka |
| 2021 | Unifying Decidable Entailments in Separation Logic with Inductive Definitions. | Mnacho Echenim, Radu Iosif, Nicolas Peltier |
| 2021 | A Unifying Splitting Framework. | Gabriel Ebner, Jasmin Blanchette, Sophie Tourret |
| 2021 | Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning. | Alessandro Cimatti, Alberto Griggio, Gianluca Redondi |
| 2021 | Subformula Linking for Intuitionistic Logic with Application to Type Theory. | Kaustuv Chaudhuri |
| 2021 | Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. | Randal E. Bryant, Marijn J. H. Heule |
| 2021 | The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints. | Franz Braue, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Mller |
| 2021 | Superposition for Full Higher-order Logic. | Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic |