| 2001 | A General Method for Using Schematizations in Automated Deduction. Nicolas Peltier |
| 2001 | A Model-Based Completeness Proof of Extended Narrowing and Resolution. Jürgen Stuber |
| 2001 | A New Meta-complexity Theorem for Bottom-Up Logic Programs. Harald Ganzinger, David A. McAllester |
| 2001 | A New System and Methodology for Generating Random Modal Formulae. Peter F. Patel-Schneider, Roberto Sebastiani |
| 2001 | A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality. Hans de Nivelle, Ian Pratt-Hartmann |
| 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 | A Top-Down Procedure for Disjunctive Well-Founded Semantics. Kewen Wang |
| 2001 | Algorithms, Datastructures, and other Issues in Efficient Automated Deduction. Andrei Voronkov |
| 2001 | Approximating Dependency Graphs Using Tree Automata Techniques. Aart Middeldorp |
| 2001 | Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems. Xavier Urbain |
| 2001 | Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings Rajeev Goré, Alexander Leitsch, Tobias Nipkow |
| 2001 | Bunched Logic Programming. Pablo A. Armelín, David J. Pym |
| 2001 | CCE: Testing Ground Joinability. Jürgen Avenhaus, Bernd Löchner |
| 2001 | Canonical Propositional Gentzen-Type Systems. Arnon Avron, Iddo Lev |
| 2001 | Combination of Distributed Search and Multi-search in Peers-mcd.d. Maria Paola Bonacina |
| 2001 | Conditional Pure Literal Graphs. Marco Benedetti |
| 2001 | Context Trees. Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela |
| 2001 | DCTP - A Disconnection Calculus Theorem Prover - System Abstract. Reinhold Letz, Gernot Stenz |
| 2001 | Decidability and Complexity of Finitely Closable Linear Equational Theories. Christopher Lynch, Barbara Morawska |
| 2001 | Decidable Classes of Inductive Theorems. Jürgen Giesl, Deepak Kapur |
| 2001 | Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL. Regimantas Pliuskevicius |
| 2001 | Deriving Modular Programs from Short Proofs. Uwe Egly, Stephan Schmitt |
| 2001 | Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability. Enrico Giunchiglia, Marco Maratea, Armando Tacchella, Davide Zambonin |
| 2001 | Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics. Volker Haarslev, Ralf Möller, Anni-Yasmin Turhan |
| 2001 | Flaw Detection in Formal Specifications. Wolfgang Reif, Gerhard Schellhorn, Andreas Thums |
| 2001 | Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation. Serenella Cerrito, Marta Cialdea Mayer |
| 2001 | Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory. Jörg Lücke |
| 2001 | Incremental Closure of Free Variable Tableaux. Martin Giese |
| 2001 | Instructing Equational Set-Reasoning with Otter. Andrea Formisano, Eugenio G. Omodeo, Marco Temperini |
| 2001 | JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants. Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin |
| 2001 | Lotrec : The Generic Tableau Prover for Modal and Description Logics. Luis Fariñas del Cerro, David Fauthoux, Olivier Gasquet, Andreas Herzig, Dominique Longin, Fabio Massacci |
| 2001 | MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction. Dominique Pastre |
| 2001 | More On Implicit Syntax. Marko Luther |
| 2001 | NEXPTIME-Complete Description Logics with Concrete Domains. Carsten Lutz |
| 2001 | NP-Completeness of Refutability by Literal-Once Resolution. Stefan Szeider |
| 2001 | NoMoRe : A System for Non-monotonic Reasoning with Logic Programs under Answer Set Semantics. Christian Anger, Kathrin Konczak, Thomas Linke |
| 2001 | On the Evaluation of Indexing Techniques for Theorem Proving. Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov |
| 2001 | On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables. Bernard Boigelot, Sébastien Jodogne, Pierre Wolper |
| 2001 | Ordered Resolution vs. Connection Graph Resolution. Reiner Hähnle, Neil V. Murray, Erik Rosenthal |
| 2001 | P.rex: An Interactive Proof Explainer. Armin Fiedler |
| 2001 | Preferred Extensions of Argumentation Frameworks: Query Answering and Computation. Sylvie Doutre, Jérôme Mengin |
| 2001 | Program Termination Analysis by Size-Change Graphs (Abstract). Neil D. Jones |
| 2001 | QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability. Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
| 2001 | RACER System Description. Volker Haarslev, Ralf Möller |
| 2001 | SET Cardholder Registration: The Secrecy Proofs. Lawrence C. Paulson |
| 2001 | STRIP: Structural Sharing for Efficient Proof-Search. Dominique Larchey-Wendling, Daniel Méry, Didier Galmiche |
| 2001 | Superposition and Chaining for Totally Ordered Divisible Abelian Groups. Uwe Waldmann |
| 2001 | System Abstract: E 0.61. Stephan Schulz |
| 2001 | System Description: RDL : Rewrite and Decision Procedure Laboratory. Alessandro Armando, Luca Compagna, Silvio Ranise |
| 2001 | System Description: SCOTT-5. Kahlil Hodgson, John K. Slaney |
| 2001 | Tableaux for Temporal Description Logic with Constant Domains. Carsten Lutz, Holger Sturm, Frank Wolter, Michael Zakharyaschev |
| 2001 | Termination and Reduction Checking for Higher-Order Logic Programs. Brigitte Pientka |
| 2001 | The Description Logic ALCNH Volker Haarslev, Ralf Möller, Michael Wessel |
| 2001 | The Hybrid µ-Calculus. Ulrike Sattler, Moshe Y. Vardi |
| 2001 | The Inverse Method Implements the Automata Approach for Modal Satisfiability. Franz Baader, Stephan Tobies |
| 2001 | The MODPROF Theorem Prover. Jens Happe |
| 2001 | The eXtended Least Number Heuristic. Gilles Audemard, Laurent Henocque |
| 2001 | Vampire 1.1 (System Description). Alexandre Riazanov, Andrei Voronkov |
| 2001 | lolliCop - A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic. Joshua S. Hodas, Naoyuki Tamura |