| 1988 | Hyper-Chaining and Knowledge-Based Theorem Proving. | Larry M. Hines |
| 1988 | Implementing Verification Strategies in the KIV-System. | Maritta Heisel, Wolfgang Reif, Werner Stephan |
| 1988 | EFS - An Interactive Environment for Formal Systems. | Timothy Griffin |
| 1988 | LP: The Larch Prover. | Stephen J. Garland, John V. Guttag |
| 1988 | Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time. | Jean H. Gallier, Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder |
| 1988 | A New Approach to Universal Unification and Its Application to AC-Unification. | Mark Franzen, Lawrence J. Henschen |
| 1988 | Specifying Theorem Provers in a Higher-Order Logic Programming Language. | Amy P. Felty, Dale Miller |
| 1988 | Lambda-Prolog: An Extended Logic Programming Language. | Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov |
| 1988 | LOGICALC: An Environment for Interactive Proof Development. | D. Duchier, Drew V. McDermott |
| 1988 | Learning and Applying Generalised Solutions using Higher Order Resolution. | Michael R. Donat, Lincoln A. Wallen |
| 1988 | The CHIP System: Constraint Handling In Prolog. | Mehmet Dincbas, Pascal Van Hentenryck, Helmut Simonis, Abderrahmane Aggoun, Alexander Herold |
| 1988 | Canonical Conditional Rewrite Systems. | Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar |
| 1988 | GEOMETER: A Theorem Prover for Algebraic Geometry. | David Cyrluk, Richard M. Harris, Deepak Kapur |
| 1988 | Recursive Query Answering with Non-Horn Clauses. | Shan Chi, Lawrence J. Henschen |
| 1988 | Linear Modal Deductions. | Luis Farias del Cerro, Andreas Herzig |
| 1988 | Unification in Finite Algebras is Unitary (?). | Wolfram Bttner |
| 1988 | Notes on Prolog Program Transformations, Prolog Style, and Efficient Compilation to The Warren Abstract Machine. | Ralph Butler, Rasiah Loganantharaj, Robert Olson |
| 1988 | Exploitation of Parallelism in Prototypical Deduction Problems. | Ralph Butler, Nicholas T. Karonis |
| 1988 | Solving Disequations in Equational Theories. | Hans-Jrgen Brckert |
| 1988 | The Use of Explicit Plans to Guide Inductive Proofs. | Alan Bundy |
| 1988 | ZPLAN: An Automatic Reasoning System for Situations. | Frank M. Brown, Seung S. Park, Jim Phelps |
| 1988 | SYMEVAL: A Theorem Prover Based on the Experimental Logic. | Frank M. Brown, Seung S. Park |
| 1988 | Analogical Reasoning and Proof Discovery. | Bishop Brock, Shaun Cooper, William Pierce |
| 1988 | Partial Unification for Graph Based Equational Reasoning. | Karl-Hans Blsius, Jrg H. Siekmann |
| 1988 | MOLOG: a Modal PROLOG. | Pierre Bieber, Luis Farias del Cerro, Andreas Herzig |