| 2000 | System Description: Interactive Proof Critics in XBarnacle. | Mike Jackson, Helen Lowe |
| 2000 | Reasoning with Individuals for the Description Logic SHIQ. | Ian Horrocks, Ulrike Sattler, Stephan Tobies |
| 2000 | Efficient Minimal Model Generation Using Branching Lemmas. | Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura |
| 2000 | High-Level Verification Using Theorem Proving and Formalized Mathematics. | John Harrison |
| 2000 | System Description: *SAT: A Platform for the Development of Modal Decision Procedures. | Enrico Giunchiglia, Armando Tacchella |
| 2000 | A Formalization of a Concurrent Object Calculus up to alpha-Conversion. | Guillaume Gillard |
| 2000 | Eliminating Dummy Elimination. | Jrgen Giesl, Aart Middeldorp |
| 2000 | Rewriting for Cryptographic Protocol Verification. | Thomas Genet, Francis Klay |
| 2000 | Workshop: Type-Theoretic Languages: Proof-Search and Semantics. | Didier Galmiche |
| 2000 | System Description: MBASE, an Open Mathematical Knowledge Base. | Andreas Franke, Michael Kohlhase |
| 2000 | An Infrastructure for Intertheory Reasoning. | William M. Farmer |
| 2000 | Reducing Model Checking of the Many to the Few. | E. Allen Emerson, Vineet Kahlon |
| 2000 | Stratified Resolution. | Anatoli Degtyarev, Andrei Voronkov |
| 2000 | Workshop: The Role of Automated Deduction in Mathematics. | Simon Colton, Volker Sorge, Ursula Martin |
| 2000 | System Description: Embedding Verification into Microsoft Excel. | Graham Collins, Louise A. Dennis |
| 2000 | ZRES: The Old Davis-Putman Procedure Meets ZBDD. | Philippe Chatalic, Laurent Simon |
| 2000 | Simulation Based Minimization. | Doron Bustan, Orna Grumberg |
| 2000 | System Description: PTTP+GLiDes: Semantically Guided PTTP. | Marianne Brown, Geoff Sutcliffe |
| 2000 | Complete Monotonic Semantic Path Orderings. | Cristina Borralleras, Maria Ferreira, Albert Rubio |
| 2000 | Automated Proof Construction in Type Theory Using Resolution. | Marc Bezem, Dimitri Hendriks, Hans de Nivelle |
| 2000 | Gdel's Algorithm for Class Formation. | Johan G. F. Belinfante |
| 2000 | Workshop: Model Computation - Principles, Algorithms, Applications. | Peter Baumgartner, Christian G. Fermller, Nicolas Peltier, Hantao Zhang |
| 2000 | FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure. | Peter Baumgartner |
| 2000 | A Framework for Cooperating Decision Procedures. | Clark W. Barrett, David L. Dill, Aaron Stump |
| 2000 | Abstract Congruence Closure and Specializations. | Leo Bachmair, Ashish Tiwari |