| 2021 | Neural Precedence Recommender. | Filip Brtek, Martin Suda |
| 2021 | Non-clausal Redundancy Properties. | Lee A. Barnett, Armin Biere |
| 2021 | Computing Optimal Repairs of Quantified ABoxes w.r.t. Static | Franz Baader, Patrick Koopmann, Francesco Kriegel, Adrian Nuradiansyah |
| 2021 | Finding Good Proofs for Description Logic Entailments using Recursive Quality Measures. | Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, Alisa Kovtunova |
| 2021 | Politeness and Stable Infiniteness: Stronger Together. | Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | Multi-Dimensional Interpretations for Termination of Term Rewriting. | Akihisa Yamada |
| 2021 | Equational Theorem Proving Modulo. | Dohan Kim, Christopher Lynch |
| 2021 | The Fusemate Logic Programming System. | Peter Baumgartner |
| 2021 | Improving ENIGMA-style Clause Selection while Learning From History. | Martin Suda |
| 2021 | Non-well-founded Deduction for Induction and Coinduction. | Liron Cohen |
| 2020 | Prolog Technology Reinforcement Learning Prover - (System Description). | Zsolt Zombori, Josef Urban, Chad E. Brown |
| 2020 | Querying the Guarded Fragment via Resolution (Extended Abstract). | Sen Zheng, Renate A. Schmidt |
| 2020 | Mechanised Modal Model Theory. | Yiming Xu, Michael Norrish |
| 2020 | A Comprehensive Framework for Saturation Theorem Proving. | Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette |
| 2020 | Boolean Reasoning in a Higher-Order Superposition Prover. | Petar Vukmirovic, Visa Nummelin |
| 2020 | Algebraically Closed Fields in Isabelle/HOL. | Paulo Emlio de Vilhena, Lawrence C. Paulson |
| 2020 | GeoGebra and the | Rbert Vajda, Zoltn Kovcs |
| 2020 | Validating Mathematical Structures. | Kazuhiko Sakaguchi |
| 2020 | Cutting Down the TPTP Language (And Others). | Nahku Saidy, Hanna Siegfried, Stephan Schulz, Geoff Sutcliffe |
| 2020 | Efficient Implementation of Large-Scale Watchlists. | Constantin Ruhdorfer, Stephan Schulz |
| 2020 | A Decision Procedure for String to Code Point Conversion. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2020 | Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. | Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli |
| 2020 | Sequoia: A Playground for Logicians - (System Description). | Giselle Reis, Zan Naeem, Mohammed Hashim |
| 2020 | Directed Graph Networks for Logical Reasoning (Extended Abstract). | Michael Rawson, Giles Reger |
| 2020 | Verification of Closest Pair of Points Algorithms. | Martin Rau, Tobias Nipkow |