| 1988 | Unification in a Combination of Arbitrary Disjoint Equational Theories. | Manfred Schmidt-Schau |
| 1988 | A Restriction of Factoring in Binary Resolution. | Arkady Rabinov |
| 1988 | Term Rewriting: Some Experimental Results. | Richard C. Potter, David A. Plaisted |
| 1988 | A Goal Directed Theorem Prover. | David A. Plaisted |
| 1988 | Single Axioms in the Implicational Propositional Calculus. | Frank Pfenning |
| 1988 | Isabelle: The Next Seven Hundred Theorem Provers. | Lawrence C. Paulson |
| 1988 | m-NEVER System Summary. | Bill Pase, Sentot Kromodimoeljo |
| 1988 | A Resolution Calculus for Modal Logics. | Hans Jrgen Ohlbach |
| 1988 | Decision Procedure for Autoepistemic Logic. | Ilkka Niemel |
| 1988 | An Implementation of a Dissolution-Based System Employing Theory Links. | Neil V. Murray, Erik Rosenthal |
| 1988 | A Decision Procedure for Unquantified Formulas of Graph Theory. | Louise E. Moser |
| 1988 | Procedural Interpretation of Non-Horn Logic Programs. | Jack Minker, Arcot Rajasekar |
| 1988 | Towards Efficient "Knowledge-Based" Automated Theorem Proving for Non-Standard Logics. | Michael A. McRobbie, Robert K. Meyer, Paul B. Thistlewaite |
| 1988 | Challenge Equality Problems in Lattice Theory. | William McCune |
| 1988 | Ontic: A Knowledge Representation System for Mathematics. | David A. McAllester |
| 1988 | Two Automated Methods in Implementation Proofs. | Leo Marcus, Timothy Redmond |
| 1988 | SATCHMO: A Theorem Prover Implemented in Prolog. | Rainer Manthey, Franois Bry |
| 1988 | Logical Matrix Generation and Testing. | Peter K. Malkin, Errol P. Martin |
| 1988 | Adventures in Associative-Commutative Unification (A Summary). | Patrick Lincoln, Jim Christian |
| 1988 | On Word Problems in Horn Theories. | Emmanuel Kounalis, Michal Rusinowitch |
| 1988 | An Interactive Enhancement to the Boyer-Moore Theorem Prover. | Matt Kaufmann |
| 1988 | RRL: A Rewrite Rule Laboratory. | Deepak Kapur, Hantao Zhang |
| 1988 | Reasoning about Systems of Linear Inequalities. | Thomas Kufl |
| 1988 | Program Synthesis by Completion with Dependent Subtypes. | Paul Jacquet |
| 1988 | Computational Metatheory in Nuprl. | Douglas J. Howe |