| 1998 | A Certified Version of Buchberger's Algorithm. Laurent Théry |
| 1998 | A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. Jacques D. Fleuriot, Lawrence C. Paulson |
| 1998 | A Fast Algorithm for Uniform Semi-Unification. Alberto Oliart, Wayne Snyder |
| 1998 | A Proof Environment for the Development of Group Communication Systems. Christoph Kreitz, Mark Hayden, Jason Hickey |
| 1998 | A Resolution Decision Procedure for the Guarded Fragment. Hans de Nivelle |
| 1998 | ACL2 Support for Verification Projects (Invited Talk). Matt Kaufmann |
| 1998 | About the Confluence of Equational Pattern Rewrite Systems. Alexandre Boudet, Evelyne Contejean |
| 1998 | Admissibility of Fixpoint Induction over Partial Types. Karl Crary |
| 1998 | Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings Claude Kirchner, Hélène Kirchner |
| 1998 | Automated Deduction of Finite-State Control Programs for Reactive Systems. Robi Malik |
| 1998 | Automated Theorem Proving in a Simple Meta-Logic for LF. Carsten Schürmann, Frank Pfenning |
| 1998 | Combining Hilbert Style and Semantic Reasoning in a Resolution Framework. Hans Jürgen Ohlbach |
| 1998 | Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk). Amir Pnueli |
| 1998 | Elimination of Equality via Transformation with Ordering Constraints. Leo Bachmair, Harald Ganzinger, Andrei Voronkov |
| 1998 | Extensional Higher-Order Resolution. Christoph Benzmüller, Michael Kohlhase |
| 1998 | On Generating Small Clause Normal Forms. Andreas Nonnengart, Georg Rock, Christoph Weidenbach |
| 1998 | On the Relationship Between Non-Horn Magic Sets and Relevancy Testing. Yoshihiko Ohta, Katsumi Inoue, Ryuzo Hasegawa |
| 1998 | Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules. Stéphane Fèvre, Dongming Wang |
| 1998 | Rank/Activity: A Canonical Form for Binary Resolution. Joseph Douglas Horton, Bruce Spencer |
| 1998 | Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). Frank Pfenning |
| 1998 | Selectively Instantiating Definitions. Matthew Bishop, Peter B. Andrews |
| 1998 | Strict Basic Superposition. Leo Bachmair, Harald Ganzinger |
| 1998 | Superposition for Divisible Torsion-Free Abelian Groups. Uwe Waldmann |
| 1998 | System Description: Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt |
| 1998 | System Description: Bernhard Beckert, Rajeev Goré |
| 1998 | System Description: An Equational Constraints Solver. Nicolas Peltier |
| 1998 | System Description: An Interface Between CL Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy |
| 1998 | System Description: CRIL Platform for SAT. Bertrand Mazure, Lakhdar Sais, Éric Grégoire |
| 1998 | System Description: Cooperation in Model Elimination: CPTHEO. Marc Fuchs, Andreas Wolf |
| 1998 | System Description: LEO - A Higher-Order Theorem Prover. Christoph Benzmüller, Michael Kohlhase |
| 1998 | System Description: Proof Planning in Higher-Order Logic with Lambda-Clam. Julian Richardson, Alan Smaill, Ian Green |
| 1998 | System Description: Similarity-Based Lemma Generation for Model Elimination. Marc Fuchs |
| 1998 | System Description: Verification of Distributed Erlang Programs. Thomas Arts, Mads Dam, Lars-Åke Fredlund, Dilian Gurov |
| 1998 | Termination Analysis by Inductive Evaluation. Jürgen Brauburger, Jürgen Giesl |
| 1998 | Towards Efficient Subsumption. Tanel Tammet |
| 1998 | Unification in Lambda-Calculi with if-then-else. Michael Beeson |
| 1998 | Using Matings for Pruning Connection Tableaux. Reinhold Letz |
| 1998 | X.R.S : Explicit Reduction Systems - A First-Order Calculus for Higher-Order Calculi. Bruno Pagano |