| 2001 | CCE: Testing Ground Joinability. | Jrgen Avenhaus, Bernd Lchner |
| 2001 | The eXtended Least Number Heuristic. | Gilles Audemard, Laurent Henocque |
| 2001 | Bunched Logic Programming. | Pablo A. Armeln, David J. Pym |
| 2001 | System Description: RDL : Rewrite and Decision Procedure Laboratory. | Alessandro Armando, Luca Compagna, Silvio Ranise |
| 2001 | NoMoRe : A System for Non-monotonic Reasoning with Logic Programs under Answer Set Semantics. | Christian Anger, Kathrin Konczak, Thomas Linke |
| 2000 | Rigid | Ashish Tiwari, Leo Bachmair, Harald Rue |
| 2000 | System Description: SystemOn TPTP. | Geoff Sutcliffe |
| 2000 | Support Ordered Resolution. | Bruce Spencer, Joseph Douglas Horton |
| 2000 | On Unification for Bonded Distributive Lattices. | Viorica Sofronie-Stokkermans |
| 2000 | Wellfounded Schematic Definitions. | Konrad Slind |
| 2000 | System Description: ARA - An Automatic Theorem Prover for Relation Algebras. | Carsten Sinz |
| 2000 | Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice. | Carl-Johan H. Seger |
| 2000 | Workshop: Automation of Proofs by Mathematical Induction. | Carsten Schrmann |
| 2000 | Tutorial: Meta-logical Frameworks. | Carsten Schrmann |
| 2000 | A Resolution Decision Procedure for Fluted Logic. | Renate A. Schmidt, Ullrich Hustadt |
| 2000 | Tutorial: Automated Deduction and Natural Language Understanding. | Stephen G. Pulman |
| 2000 | System Description: DLP. | Peter F. Patel-Schneider |
| 2000 | Proof Generation in the Touchstone Theorem Prover. | George C. Necula, Peter Lee |
| 2000 | Machine Instruction Syntax and Semantics in Higher Order Logic. | Neophytos G. Michael, Andrew W. Appel |
| 2000 | Workshop: Automated Deduction in Education. | Erica Melis |
| 2000 | System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level. | Andreas Meier |
| 2000 | System Description: IVY. | William McCune, Olga Shumsky |
| 2000 | Scalable Knowledge Representation and Reasoning Systems. | Henry A. Kautz |
| 2000 | Extending Decision Procedures with Induction Schemes. | Deepak Kapur, Mahadevan Subramaniam |
| 2000 | Modular Reasoning in Isabelle. | Florian Kammller |