| 2020 | Description Logics with Concrete Domains and General Concept Inclusions Revisited. | Franz Baader, Jakub Rydval |
| 2020 | Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols. | Franz Baader, Deepak Kapur |
| 2020 | Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates. | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2020 | Formalizing the Face Lattice of Polyhedra. | Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub |
| 2020 | Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. | Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi |
| 2020 | New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract). | Erika brahm, James H. Davenport, Matthew England, Gereon Kremer, Zak Tonks |
| 2020 | NP Reasoning in the Monotone μ-Calculus. | Daniel Hausmann, Lutz Schrder |
| 2020 | Politeness for the Theory of Algebraic Datatypes. | Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett |
| 2020 | Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. | Sebastian Ullrich, Leonardo de Moura |
| 2020 | Integrating Induction and Coinduction via Closure Operators and Proof Cycles. | Liron Cohen, Reuben N. S. Rowe |
| 2020 | Teaching Automated Theorem Proving by Example: PyRes 1.2 - (System Description). | Stephan Schulz, Adam Pease |
| 2020 | Practical Proof Search for Coq by Type Inhabitation. | Lukasz Czajka |
| 2020 | Possible Models Computation and Revision - A Practical Approach. | Peter Baumgartner |
| 2019 | FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. | Yizheng Zhao, Renate A. Schmidt |
| 2019 | Optimization Modulo the Theory of Floating-Point Numbers. | Patrick Trentin, Roberto Sebastiani |
| 2019 | GKC: A Reasoning System for Large Knowledge Bases. | Tanel Tammet |
| 2019 | JGXYZ: An ATP System for Gap and Glut Logics. | Geoff Sutcliffe, Francis Jeffry Pelletier |
| 2019 | Certified Equational Reasoning via Ordered Completion. | Christian Sternagel, Sarah Winkler |
| 2019 | Induction in Saturation-Based Proof Search. | Giles Reger, Andrei Voronkov |
| 2019 | Old or Heavy? Decaying Gracefully with Age/Weight Shapes. | Michael Rawson, Giles Reger |
| 2019 | Uniform Substitution at One Fell Swoop. | Andr Platzer |
| 2019 | The Aspect Calculus. | David A. Plaisted |
| 2019 | On Invariant Synthesis for Parametric Systems. | Dennis Peuter, Viorica Sofronie-Stokkermans |
| 2019 | Towards Bit-Width-Independent Proofs in SMT Solvers. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli |
| 2019 | On the Width of Regular Classes of Finite Structures. | Alexsander Andrade de Melo, Mateus de Oliveira Oliveira |