| 2000 | Two Techniques to Improve Finite Model Search. | Gilles Audemard, Belaid Benhamou, Laurent Henocque |
| 2000 | System Description: TPS: A Theorem Proving System for Type Theory. | Peter B. Andrews, Matthew Bishop, Chad E. Brown |
| 2000 | Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. | Peter B. Andrews, Chad E. Brown |
| 2000 | The Nuprl Open Logical Environment. | Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo |
| 1999 | System Description: MCS: Model-based Conjecture Searching. | Jian Zhang |
| 1999 | Complexity of the higher order matching. | Tomasz Wierzbicki |
| 1999 | System Description: CyNTHIA. | Jon Whittle, Alan Bundy, Richard J. Boulton, Helen Lowe |
| 1999 | System Description: Spass Version 1.0.0. | Christoph Weidenbach |
| 1999 | Towards an Automatic Analysis of Security Protocols in First-Order Logic. | Christoph Weidenbach |
| 1999 | KK: a theorem prover for K. | Andrei Voronkov |
| 1999 | A PSpace Algorithm for Graded Modal Logic. | Stephan Tobies |
| 1999 | On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results. | Viorica Sofronie-Stokkermans |
| 1999 | System Abstract: E 0.3. | Stephan Schulz |
| 1999 | Solvability of Context Equations with Two Context Variables is Decidable. | Manfred Schmidt-Schau, Klaus U. Schulz |
| 1999 | Vampire. | Alexandre Riazanov, Andrei Voronkov |
| 1999 | A formalization of Static Analyses in System F. | Frdric Prost |
| 1999 | Solving Equational Problems Efficiently. | Reinhard Pichler |
| 1999 | System Description: Twelf - A Meta-Logical Framework for Deductive Systems. | Frank Pfenning, Carsten Schrmann |
| 1999 | Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract). | Tobias Nipkow |
| 1999 | Invited Talk: Rewrite-based Deduction and Symbolic Constraints. | Robert Nieuwenhuis |
| 1999 | System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog. | Gopalan Nadathur, Dustin J. Mitchell |
| 1999 | Automatic Generation of Proof Search Strategies for Second-order Logic. | Raul H. C. Lopes |
| 1999 | System Description: Kimba, A Model Generator for Many-Valued First-Order Logics. | Karsten Konrad, David A. Wolfram |
| 1999 | A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers. | Predrag Janicic, Alan Bundy, Ian Green |
| 1999 | The Design of the CADE-16 Inductive Theorem Prover Contest. | Dieter Hutter, Alan Bundy |