| 2001 | NP-Completeness of Refutability by Literal-Once Resolution. | Stefan Szeider |
| 2001 | A Model-Based Completeness Proof of Extended Narrowing and Resolution. | Jrgen Stuber |
| 2001 | System Abstract: E 0.61. | Stephan Schulz |
| 2001 | JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants. | Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin |
| 2001 | The Hybrid µ-Calculus. | Ulrike Sattler, Moshe Y. Vardi |
| 2001 | Vampire 1.1 (System Description). | Alexandre Riazanov, Andrei Voronkov |
| 2001 | Flaw Detection in Formal Specifications. | Wolfgang Reif, Gerhard Schellhorn, Andreas Thums |
| 2001 | Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL. | Regimantas Pliuskevicius |
| 2001 | Termination and Reduction Checking for Higher-Order Logic Programs. | Brigitte Pientka |
| 2001 | A General Method for Using Schematizations in Automated Deduction. | Nicolas Peltier |
| 2001 | SET Cardholder Registration: The Secrecy Proofs. | Lawrence C. Paulson |
| 2001 | A New System and Methodology for Generating Random Modal Formulae. | Peter F. Patel-Schneider, Roberto Sebastiani |
| 2001 | MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction. | Dominique Pastre |
| 2001 | A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality. | Hans de Nivelle, Ian Pratt-Hartmann |
| 2001 | On the Evaluation of Indexing Techniques for Theorem Proving. | Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov |
| 2001 | Approximating Dependency Graphs Using Tree Automata Techniques. | Aart Middeldorp |
| 2001 | Decidability and Complexity of Finitely Closable Linear Equational Theories. | Christopher Lynch, Barbara Morawska |
| 2001 | Tableaux for Temporal Description Logic with Constant Domains. | Carsten Lutz, Holger Sturm, Frank Wolter, Michael Zakharyaschev |
| 2001 | NEXPTIME-Complete Description Logics with Concrete Domains. | Carsten Lutz |
| 2001 | More On Implicit Syntax. | Marko Luther |
| 2001 | Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory. | Jrg Lcke |
| 2001 | DCTP - A Disconnection Calculus Theorem Prover - System Abstract. | Reinhold Letz, Gernot Stenz |
| 2001 | STRIP: Structural Sharing for Efficient Proof-Search. | Dominique Larchey-Wendling, Daniel Mry, Didier Galmiche |
| 2001 | Program Termination Analysis by Size-Change Graphs (Abstract). | Neil D. Jones |
| 2001 | System Description: SCOTT-5. | Kahlil Hodgson, John K. Slaney |