| 2020 | Make E Smart Again (Short Paper). | Zarathustra Amadeus Goertzel |
| 2020 | Subsumption Demodulation in First-Order Theorem Proving. | Bernhard Gleiss, Laura Kovcs, Jakob Rath |
| 2020 | Layered Clause Selection for Saturation-Based Theorem Proving. | Bernhard Gleiss, Martin Suda |
| 2020 | Layered Clause Selection for Theory Reasoning - (Short Paper). | Bernhard Gleiss, Martin Suda |
| 2020 | MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description). | Marianna Girlando, Lutz Straburger |
| 2020 | Quotients of Bounded Natural Functors. | Basil Frer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel |
| 2020 | Formalizing a Seligman-Style Tableau System for Hybrid Logic - (Short Paper). | Asta Halkjr From, Patrick Blackburn, Jrgen Villadsen |
| 2020 | Verified Approximation Algorithms. | Robin Emann, Tobias Nipkow, Simon Robillard |
| 2020 | Implementing Superposition in iProver (System Description). | Andr Duarte, Konstantin Korovin |
| 2020 | HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description). | Tiziano Dalmonte, Nicola Olivetti, Gian Luca Pozzato |
| 2020 | How QBF Expansion Makes Strategy Extraction Hard. | Leroy Chew, Judith Clymo |
| 2020 | Combined Covers and Beth Definability. | Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin |
| 2020 | N-PAT: A Nested Model-Checker - (System Description). | Hadrien Bride, Cheng-Hao Cai, Jin Song Dong, Rajeev Gor, Zh Hu, Brendan P. Mahony, Jim McCarthy |
| 2020 | The Resolution of Keller's Conjecture. | Joshua Brakensiek, Marijn Heule, John Mackey, David E. Narvez |
| 2020 | SGGS Decision Procedures. | Maria Paola Bonacina, Sarah Winkler |
| 2020 | Constructive Hybrid Games. | Rose Bohrer, Andr Platzer |
| 2020 | A Polymorphic Vampire - (Short Paper). | Ahmed Bhayat, Giles Reger |
| 2020 | A Combinator-Based Superposition Calculus for Higher-Order Logic. | Ahmed Bhayat, Giles Reger |
| 2020 | A Knuth-Bendix-Like Ordering for Orienting Combinator Equations. | Ahmed Bhayat, Giles Reger |
| 2020 | A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic. | David A. Basin, Thibault Dardinier, Lukas Heimes, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel |
| 2020 | Learning Precedences from Simple Symbol Features. | Filip Brtek, Martin Suda |
| 2020 | Animated Logic: Correct Functional Conversion to Conjunctive Normal Form. | Pedro Barroso, Mrio Pereira, Antnio Ravara |
| 2020 | Covered Clauses Are Not Propagation Redundant. | Lee A. Barnett, David M. Cerna, Armin Biere |
| 2020 | An SMT Theory of Fixed-Point Arithmetic. | Marek S. Baranowski, Shaobo He, Mathias Lechner, Thanh Son Nguyen, Zvonimir Rakamaric |
| 2020 | A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper). | Anne Baanen |