| 1998 | Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk). | Amir Pnueli |
| 1998 | Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). | Frank Pfenning |
| 1998 | System Description: An Equational Constraints Solver. | Nicolas Peltier |
| 1998 | X.R.S : Explicit Reduction Systems - A First-Order Calculus for Higher-Order Calculi. | Bruno Pagano |
| 1998 | A Fast Algorithm for Uniform Semi-Unification. | Alberto Oliart, Wayne Snyder |
| 1998 | On the Relationship Between Non-Horn Magic Sets and Relevancy Testing. | Yoshihiko Ohta, Katsumi Inoue, Ryuzo Hasegawa |
| 1998 | Combining Hilbert Style and Semantic Reasoning in a Resolution Framework. | Hans Jrgen Ohlbach |
| 1998 | On Generating Small Clause Normal Forms. | Andreas Nonnengart, Georg Rock, Christoph Weidenbach |
| 1998 | A Resolution Decision Procedure for the Guarded Fragment. | Hans de Nivelle |
| 1998 | System Description: CRIL Platform for SAT. | Bertrand Mazure, Lakhdar Sais, ric Grgoire |
| 1998 | Automated Deduction of Finite-State Control Programs for Reactive Systems. | Robi Malik |
| 1998 | Using Matings for Pruning Connection Tableaux. | Reinhold Letz |
| 1998 | A Proof Environment for the Development of Group Communication Systems. | Christoph Kreitz, Mark Hayden, Jason Hickey |
| 1998 | ACL2 Support for Verification Projects (Invited Talk). | Matt Kaufmann |
| 1998 | Rank/Activity: A Canonical Form for Binary Resolution. | Joseph Douglas Horton, Bruce Spencer |
| 1998 | System Description: | Rajeev Gor, Joachim Posegga, Andrew Slater, Harald Vogt |
| 1998 | System Description: Cooperation in Model Elimination: CPTHEO. | Marc Fuchs, Andreas Wolf |
| 1998 | System Description: Similarity-Based Lemma Generation for Model Elimination. | Marc Fuchs |
| 1998 | A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. | Jacques D. Fleuriot, Lawrence C. Paulson |
| 1998 | Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules. | Stphane Fvre, Dongming Wang |
| 1998 | Admissibility of Fixpoint Induction over Partial Types. | Karl Crary |
| 1998 | Termination Analysis by Inductive Evaluation. | Jrgen Brauburger, Jrgen Giesl |
| 1998 | About the Confluence of Equational Pattern Rewrite Systems. | Alexandre Boudet, Evelyne Contejean |
| 1998 | Selectively Instantiating Definitions. | Matthew Bishop, Peter B. Andrews |
| 1998 | System Description: LEO - A Higher-Order Theorem Prover. | Christoph Benzmller, Michael Kohlhase |