| 2001 | lolliCop - A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic. | Joshua S. Hodas, Naoyuki Tamura |
| 2001 | The MODPROF Theorem Prover. | Jens Happe |
| 2001 | Ordered Resolution vs. Connection Graph Resolution. | Reiner Hhnle, Neil V. Murray, Erik Rosenthal |
| 2001 | The Description Logic ALCNH | Volker Haarslev, Ralf Mller, Michael Wessel |
| 2001 | Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics. | Volker Haarslev, Ralf Mller, Anni-Yasmin Turhan |
| 2001 | RACER System Description. | Volker Haarslev, Ralf Mller |
| 2001 | QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability. | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
| 2001 | Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability. | Enrico Giunchiglia, Marco Maratea, Armando Tacchella, Davide Zambonin |
| 2001 | Decidable Classes of Inductive Theorems. | Jrgen Giesl, Deepak Kapur |
| 2001 | Incremental Closure of Free Variable Tableaux. | Martin Giese |
| 2001 | Context Trees. | Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela |
| 2001 | A New Meta-complexity Theorem for Bottom-Up Logic Programs. | Harald Ganzinger, David A. McAllester |
| 2001 | Instructing Equational Set-Reasoning with Otter. | Andrea Formisano, Eugenio G. Omodeo, Marco Temperini |
| 2001 | P.rex: An Interactive Proof Explainer. | Armin Fiedler |
| 2001 | Deriving Modular Programs from Short Proofs. | Uwe Egly, Stephan Schmitt |
| 2001 | Preferred Extensions of Argumentation Frameworks: Query Answering and Computation. | Sylvie Doutre, Jrme Mengin |
| 2001 | Lotrec : The Generic Tableau Prover for Modal and Description Logics. | Luis Farias del Cerro, David Fauthoux, Olivier Gasquet, Andreas Herzig, Dominique Longin, Fabio Massacci |
| 2001 | Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation. | Serenella Cerrito, Marta Cialdea Mayer |
| 2001 | Combination of Distributed Search and Multi-search in Peers-mcd.d. | Maria Paola Bonacina |
| 2001 | On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables. | Bernard Boigelot, Sbastien Jodogne, Pierre Wolper |
| 2001 | Conditional Pure Literal Graphs. | Marco Benedetti |
| 2001 | A Second-Order Theorem Prover Applied to Circumscription. | Michael Beeson |
| 2001 | A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities. | Bernhard Beckert, Steffen Schlager |
| 2001 | The Inverse Method Implements the Automata Approach for Modal Satisfiability. | Franz Baader, Stephan Tobies |
| 2001 | Canonical Propositional Gentzen-Type Systems. | Arnon Avron, Iddo Lev |