| 2000 | A Formalization of a Concurrent Object Calculus up to alpha-Conversion. Guillaume Gillard |
| 2000 | A Framework for Cooperating Decision Procedures. Clark W. Barrett, David L. Dill, Aaron Stump |
| 2000 | A Resolution Decision Procedure for Fluted Logic. Renate A. Schmidt, Ullrich Hustadt |
| 2000 | Abstract Congruence Closure and Specializations. Leo Bachmair, Ashish Tiwari |
| 2000 | An Infrastructure for Intertheory Reasoning. William M. Farmer |
| 2000 | Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings David A. McAllester |
| 2000 | Automated Proof Construction in Type Theory Using Resolution. Marc Bezem, Dimitri Hendriks, Hans de Nivelle |
| 2000 | Complete Monotonic Semantic Path Orderings. Cristina Borralleras, Maria Ferreira, Albert Rubio |
| 2000 | Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice. Carl-Johan H. Seger |
| 2000 | Efficient Minimal Model Generation Using Branching Lemmas. Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura |
| 2000 | Eliminating Dummy Elimination. Jürgen Giesl, Aart Middeldorp |
| 2000 | Extending Decision Procedures with Induction Schemes. Deepak Kapur, Mahadevan Subramaniam |
| 2000 | FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure. Peter Baumgartner |
| 2000 | Gödel's Algorithm for Class Formation. Johan G. F. Belinfante |
| 2000 | High-Level Verification Using Theorem Proving and Formalized Mathematics. John Harrison |
| 2000 | Machine Instruction Syntax and Semantics in Higher Order Logic. Neophytos G. Michael, Andrew W. Appel |
| 2000 | Modular Reasoning in Isabelle. Florian Kammüller |
| 2000 | On Unification for Bonded Distributive Lattices. Viorica Sofronie-Stokkermans |
| 2000 | Proof Generation in the Touchstone Theorem Prover. George C. Necula, Peter Lee |
| 2000 | Reasoning with Individuals for the Description Logic SHIQ. Ian Horrocks, Ulrike Sattler, Stephan Tobies |
| 2000 | Reducing Model Checking of the Many to the Few. E. Allen Emerson, Vineet Kahlon |
| 2000 | Rewriting for Cryptographic Protocol Verification. Thomas Genet, Francis Klay |
| 2000 | Rigid Ashish Tiwari, Leo Bachmair, Harald Rueß |
| 2000 | Scalable Knowledge Representation and Reasoning Systems. Henry A. Kautz |
| 2000 | Simulation Based Minimization. Doron Bustan, Orna Grumberg |
| 2000 | Stratified Resolution. Anatoli Degtyarev, Andrei Voronkov |
| 2000 | Support Ordered Resolution. Bruce Spencer, Joseph Douglas Horton |
| 2000 | System Description: *SAT: A Platform for the Development of Modal Decision Procedures. Enrico Giunchiglia, Armando Tacchella |
| 2000 | System Description: ARA - An Automatic Theorem Prover for Relation Algebras. Carsten Sinz |
| 2000 | System Description: DLP. Peter F. Patel-Schneider |
| 2000 | System Description: Embedding Verification into Microsoft Excel. Graham Collins, Louise A. Dennis |
| 2000 | System Description: IVY. William McCune, Olga Shumsky |
| 2000 | System Description: Interactive Proof Critics in XBarnacle. Mike Jackson, Helen Lowe |
| 2000 | System Description: MBASE, an Open Mathematical Knowledge Base. Andreas Franke, Michael Kohlhase |
| 2000 | System Description: PTTP+GLiDes: Semantically Guided PTTP. Marianne Brown, Geoff Sutcliffe |
| 2000 | System Description: SystemOn TPTP. Geoff Sutcliffe |
| 2000 | System Description: TPS: A Theorem Proving System for Type Theory. Peter B. Andrews, Matthew Bishop, Chad E. Brown |
| 2000 | System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level. Andreas Meier |
| 2000 | The Nuprl Open Logical Environment. Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo |
| 2000 | Tutorial: Automated Deduction and Natural Language Understanding. Stephen G. Pulman |
| 2000 | Tutorial: Meta-logical Frameworks. Carsten Schürmann |
| 2000 | Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. Peter B. Andrews, Chad E. Brown |
| 2000 | Two Techniques to Improve Finite Model Search. Gilles Audemard, Belaid Benhamou, Laurent Henocque |
| 2000 | Wellfounded Schematic Definitions. Konrad Slind |
| 2000 | Workshop: Automated Deduction in Education. Erica Melis |
| 2000 | Workshop: Automation of Proofs by Mathematical Induction. Carsten Schürmann |
| 2000 | Workshop: Model Computation - Principles, Algorithms, Applications. Peter Baumgartner, Christian G. Fermüller, Nicolas Peltier, Hantao Zhang |
| 2000 | Workshop: The Role of Automated Deduction in Mathematics. Simon Colton, Volker Sorge, Ursula Martin |
| 2000 | Workshop: Type-Theoretic Languages: Proof-Search and Semantics. Didier Galmiche |
| 2000 | ZRES: The Old Davis-Putman Procedure Meets ZBDD. Philippe Chatalic, Laurent Simon |