| 1988 | 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings Ewing L. Lusk, Ross A. Overbeek |
| 1988 | A Decision Procedure for Unquantified Formulas of Graph Theory. Louise E. Moser |
| 1988 | A Goal Directed Theorem Prover. David A. Plaisted |
| 1988 | A Mechanizable Induction Principle for Equational Specifications. Hantao Zhang, Deepak Kapur, Mukkai S. Krishnamoorthy |
| 1988 | A New Approach to Universal Unification and Its Application to AC-Unification. Mark Franzen, Lawrence J. Henschen |
| 1988 | A Prolog Technology Theorem Prover. Mark E. Stickel |
| 1988 | A Resolution Calculus for Modal Logics. Hans Jürgen Ohlbach |
| 1988 | A Restriction of Factoring in Binary Resolution. Arkady Rabinov |
| 1988 | A Subsumption Algorithm Based on Characteristic Matrices. Rolf Socher |
| 1988 | Adventures in Associative-Commutative Unification (A Summary). Patrick Lincoln, Jim Christian |
| 1988 | An Environment For Automated Reasoning About Partial Functions. David A. Basin |
| 1988 | An Implementation of a Dissolution-Based System Employing Theory Links. Neil V. Murray, Erik Rosenthal |
| 1988 | An Interactive Enhancement to the Boyer-Moore Theorem Prover. Matt Kaufmann |
| 1988 | An nH-Prolog Implementation. Bruce T. Smith, Donald W. Loveland |
| 1988 | Analogical Reasoning and Proof Discovery. Bishop Brock, Shaun Cooper, William Pierce |
| 1988 | Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. Christoph Walther |
| 1988 | Canonical Conditional Rewrite Systems. Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar |
| 1988 | Case Inference in Resolution-Based Languages. Toshiro Wakayama, T. H. Payne |
| 1988 | Challenge Equality Problems in Lattice Theory. William McCune |
| 1988 | Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. Larry Wos, William McCune |
| 1988 | Challenge Problems from Nonassociative Rings for Theorem Provers. Rick L. Stevens |
| 1988 | Checking Natural Language Proofs. Donald Simon |
| 1988 | Computational Metatheory in Nuprl. Douglas J. Howe |
| 1988 | Consistency of Rule-based Expert System. Marc Bezem |
| 1988 | Decision Procedure for Autoepistemic Logic. Ilkka Niemelä |
| 1988 | EFS - An Interactive Environment for Formal Systems. Timothy Griffin |
| 1988 | Elements of Z-Module Reasoning. Tie-Cheng Wang |
| 1988 | Exploitation of Parallelism in Prototypical Deduction Problems. Ralph Butler, Nicholas T. Karonis |
| 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 | First-Order Theorem Proving Using Conditional Rewrite Rules. Hantao Zhang, Deepak Kapur |
| 1988 | GEOMETER: A Theorem Prover for Algebraic Geometry. David Cyrluk, Richard M. Harris, Deepak Kapur |
| 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 | Isabelle: The Next Seven Hundred Theorem Provers. Lawrence C. Paulson |
| 1988 | LOGICALC: An Environment for Interactive Proof Development. D. Duchier, Drew V. McDermott |
| 1988 | LP: The Larch Prover. Stephen J. Garland, John V. Guttag |
| 1988 | Lambda-Prolog: An Extended Logic Programming Language. Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov |
| 1988 | Learning and Applying Generalised Solutions using Higher Order Resolution. Michael R. Donat, Lincoln A. Wallen |
| 1988 | Linear Modal Deductions. Luis Fariñas del Cerro, Andreas Herzig |
| 1988 | Logical Matrix Generation and Testing. Peter K. Malkin, Errol P. Martin |
| 1988 | MOLOG: a Modal PROLOG. Pierre Bieber, Luis Fariñas del Cerro, Andreas Herzig |
| 1988 | Notes on Prolog Program Transformations, Prolog Style, and Efficient Compilation to The Warren Abstract Machine. Ralph Butler, Rasiah Loganantharaj, Robert Olson |
| 1988 | On Word Problems in Horn Theories. Emmanuel Kounalis, Michaël Rusinowitch |
| 1988 | Ontic: A Knowledge Representation System for Mathematics. David A. McAllester |
| 1988 | Optimal Time Bounds for Parallel Term Matching. Rakesh M. Verma, I. V. Ramakrishnan |
| 1988 | PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. P. E. Allen, Soumitra Bose, Edmund M. Clarke, Spiro Michaylov |
| 1988 | Partial Unification for Graph Based Equational Reasoning. Karl-Hans Bläsius, Jörg H. Siekmann |
| 1988 | Procedural Interpretation of Non-Horn Logic Programs. Jack Minker, Arcot Rajasekar |
| 1988 | Program Synthesis by Completion with Dependent Subtypes. Paul Jacquet |
| 1988 | Propositional Temporal Interval Logic is PSPACE Complete. A. A. Aaby, K. T. Narayana |
| 1988 | QUANTLOG: A System for Approximate Reasoning in Inconsistent Formal Systems. V. S. Subrahmanian, Zerksis D. Umrigar |
| 1988 | Query Processing in Quantitative Logic Programming. V. S. Subrahmanian |
| 1988 | RRL: A Rewrite Rule Laboratory. Deepak Kapur, Hantao Zhang |
| 1988 | Reasoning about Systems of Linear Inequalities. Thomas Käufl |
| 1988 | Recursive Query Answering with Non-Horn Clauses. Shan Chi, Lawrence J. Henschen |
| 1988 | SATCHMO: A Theorem Prover Implemented in Prolog. Rainer Manthey, François Bry |
| 1988 | SYMEVAL: A Theorem Prover Based on the Experimental Logic. Frank M. Brown, Seung S. Park |
| 1988 | Single Axioms in the Implicational Propositional Calculus. Frank Pfenning |
| 1988 | Solving Disequations in Equational Theories. Hans-Jürgen Bürckert |
| 1988 | Some Tools for an Inference Laboratory (ATINF). Thierry Boy de la Tour, Ricardo Caferra, Gilles Chaminade |
| 1988 | Specifying Theorem Provers in a Higher-Order Logic Programming Language. Amy P. Felty, Dale Miller |
| 1988 | Supposition-Based Logic for Automated Nonmontonic Reasoning. Philippe Besnard, Pierre Siegel |
| 1988 | Term Rewriting: Some Experimental Results. Richard C. Potter, David A. Plaisted |
| 1988 | The CHIP System: Constraint Handling In Prolog. Mehmet Dincbas, Pascal Van Hentenryck, Helmut Simonis, Abderrahmane Aggoun, Alexander Herold |
| 1988 | The KLAUS Automated Deduction System. Mark E. Stickel |
| 1988 | The TPS Theorem Proving System. Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning |
| 1988 | The Use of Explicit Plans to Guide Inductive Proofs. Alan Bundy |
| 1988 | Towards Efficient "Knowledge-Based" Automated Theorem Proving for Non-Standard Logics. Michael A. McRobbie, Robert K. Meyer, Paul B. Thistlewaite |
| 1988 | Two Automated Methods in Implementation Proofs. Leo Marcus, Timothy Redmond |
| 1988 | Type Inference in Prolog. H. Azzoune |
| 1988 | Unification in Finite Algebras is Unitary (?). Wolfram Büttner |
| 1988 | Unification in a Combination of Arbitrary Disjoint Equational Theories. Manfred Schmidt-Schauß |
| 1988 | ZPLAN: An Automatic Reasoning System for Situations. Frank M. Brown, Seung S. Park, Jim Phelps |
| 1988 | m-NEVER System Summary. Bill Pase, Sentot Kromodimoeljo |