| 1998 | Extensional Higher-Order Resolution. | Christoph Benzmller, Michael Kohlhase |
| 1998 | Unification in Lambda-Calculi with if-then-else. | Michael Beeson |
| 1998 | System Description: | Bernhard Beckert, Rajeev Gor |
| 1998 | Elimination of Equality via Transformation with Ordering Constraints. | Leo Bachmair, Harald Ganzinger, Andrei Voronkov |
| 1998 | Strict Basic Superposition. | Leo Bachmair, Harald Ganzinger |
| 1998 | System Description: Verification of Distributed Erlang Programs. | Thomas Arts, Mads Dam, Lars-ke Fredlund, Dilian Gurov |
| 1997 | SATO: An Efficient Propositional Prover. | Hantao Zhang |
| 1997 | A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple Geometry. | Lu Yang, Hongguang Fu, Zhenbing Zeng |
| 1997 | ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output. | Andreas Wolf, Johann Schumann |
| 1997 | The Char-Set Method and Its Applications to Automated Reasoning. | Wu Wen-Tsn |
| 1997 | Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics. | Moshe Y. Vardi |
| 1997 | Minlog: A Minimal Logic Theorem Prover. | John K. Slaney |
| 1997 | Automatic Verification of Cryptographic Protocols with SETHEO. | Johann Schumann |
| 1997 | Exact Kanowledge Compilation in Predicate Calculus: The Partial Achievement Case. | Olivier Roussel, Philippe Mathieu |
| 1997 | Proving System Correctness with KIV 3.0. | Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel |
| 1997 | XIsabelle: A System Description. | Maris A. Ozols, Anthony Cant, Katherine A. Eastaughffe |
| 1997 | RALL: Machine-Supported Proofs for Relation Algebra. | David von Oheimb, Thomas F. Gritzner |
| 1997 | A Classification of Non-liftable Orders for Resolution. | Hans de Nivelle |
| 1997 | Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. | Robert Nieuwenhuis, Jos Miguel Rivero, Miguel ngel Vallejo |
| 1997 | On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting. | Joachim Niehren, Manfred Pinkal, Peter Ruhrberg |
| 1997 | A Practical Implementation of Simple Consequence Relations Using Inductive Definitions. | Sen Matthews |
| 1997 | XBarnacle: Making Theorem Provers More Accessible. | Helen Lowe, David Duncan |
| 1997 | Connection-Based Proof Construction in Linear Logic. | Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt |
| 1997 | Deciding Intuitionistic Propositional Logic via Translation into Classical Logic. | Daniel S. Korn, Christoph Kreitz |
| 1997 | Plagiator - A Learning Prover. | Thomas Kolbe, Jrgen Brauburger |