| 2002 | An LCF-Style Interface between HOL and First-Order Logic. | Joe Hurd |
| 2002 | Reasoning with Expressive Description Logics: Theory and Practice. | Ian Horrocks |
| 2002 | The Next W ALDMEISTER Loop. | Thomas Hillenbrand, Bernd Lchner |
| 2002 | Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations. | Bernhard Gramlich, Reinhard Pichler |
| 2002 | Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points. | Eugene Goldberg |
| 2002 | A New Clausal Class Decidable by Hyperresolution. | Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt |
| 2002 | Shostak Light. | Harald Ganzinger |
| 2002 | Connection-Based Proof Search in Propositional BI Logic. | Didier Galmiche, Daniel Mry |
| 2002 | Formal Verification of a Combination Decision Procedure. | Jonathan Ford, Natarajan Shankar |
| 2002 | Embedding Lax Logic into Intuitionistic Logic. | Uwe Egly |
| 2002 | The HR Program for Theorem Generation. | Simon Colton |
| 2002 | Solving for Set Variables in Higher-Order Theorem Proving. | Chad E. Brown |
| 2002 | Recursive Path Orderings Can Be Context-Sensitive. | Cristina Borralleras, Salvador Lucas, Albert Rubio |
| 2002 | Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation. | Miquel Bofill, Albert Rubio |
| 2002 | Temporal Logic for Proof-Carrying Code. | Andrew Bernard, Peter Lee |
| 2002 | Proof Analysis by Resolution. | Matthias Baaz |
| 2002 | A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. | Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
| 2002 | Reasoning by Symmetry and Function Ordering in Finite Model Generation. | Gilles Audemard, Belaid Benhamou |
| 2002 | HyLoRes 1.0: Direct Resolution for Hybrid Logics. | Carlos Areces, Juan Heguiabehere |
| 2002 | Focussing Proof-Net Construction as a Middleware Paradigm. | Jean-Marc Andreoli |
| 2002 | Deductive Search for Errors in Free Data Type Specifications Using Model Generation. | Wolfgang Ahrendt |
| 2001 | A Top-Down Procedure for Disjunctive Well-Founded Semantics. | Kewen Wang |
| 2001 | Superposition and Chaining for Totally Ordered Divisible Abelian Groups. | Uwe Waldmann |
| 2001 | Algorithms, Datastructures, and other Issues in Efficient Automated Deduction. | Andrei Voronkov |
| 2001 | Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems. | Xavier Urbain |