| 1999 | Maslov's Class K Revisited. | Ullrich Hustadt, Renate A. Schmidt |
| 1999 | Presenting Proofs in a Human-Oriented Way. | Helmut Horacek |
| 1999 | System Description: Waldmeister - Improvements in Performance and Ease of Use. | Thomas Hillenbrand, Andreas Jaeger, Bernd Lchner |
| 1999 | Fault-Tolerant Distributed Theorem Proving. | Jason Hickey |
| 1999 | A dynamic programming approach to categorial deduction. | Philippe de Groote |
| 1999 | System Description: Using OBDD's for the validation of Skolem verification conditions. | E. Pascal Gribomont, Nachaat Salloum |
| 1999 | Invited Talk: Decision procedures for guarded logics. | Erich Grdel |
| 1999 | Abstraction-Based Relevancy Testing for Model Elimination. | Marc Fuchs, Dirk Fuchs |
| 1999 | System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving. | Andreas Franke, Michael Kohlhase |
| 1999 | Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems. | Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury |
| 1999 | Tractable Transformations from Modal Provability Logics into First-Order Logic. | Stphane Demri, Rajeev Gor |
| 1999 | A Breadth-First Strategy for Mating Search. | Matthew Bishop |
| 1999 | Extensional Higher-Order Paramodulation and RUE-Resolution. | Christoph Benzmller |
| 1999 | A Confluent Connection Calculus. | Peter Baumgartner, Norbert Eisinger, Ulrich Furbach |
| 1999 | System Description: CutRes 0.1: Cut Elimination by Resolution. | Matthias Baaz, Alexander Leitsch, Georg Moser |
| 1999 | System Description: inka 5.0 - A Logic Voyager. | Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer |
| 1999 | On Explicit Reflection in Theorem Proving and Formal Verification. | Sergei N. Artmov |
| 1999 | Prefixed Resolution: A Resolution Method for Modal and Description Logics. | Carlos Areces, Hans de Nivelle, Maarten de Rijke |
| 1999 | VSDITLU: a verifiable symbolic definite integral table look-up. | Andrew A. Adams, Hanne Gottliebsen, Steve Linton, Ursula Martin |
| 1998 | Superposition for Divisible Torsion-Free Abelian Groups. | Uwe Waldmann |
| 1998 | A Certified Version of Buchberger's Algorithm. | Laurent Thry |
| 1998 | Towards Efficient Subsumption. | Tanel Tammet |
| 1998 | System Description: An Interface Between CL | Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy |
| 1998 | Automated Theorem Proving in a Simple Meta-Logic for LF. | Carsten Schrmann, Frank Pfenning |
| 1998 | System Description: Proof Planning in Higher-Order Logic with Lambda-Clam. | Julian Richardson, Alan Smaill, Ian Green |