| 1988 | Consistency of Rule-based Expert System. | Marc Bezem |
| 1988 | Supposition-Based Logic for Automated Nonmontonic Reasoning. | Philippe Besnard, Pierre Siegel |
| 1988 | An Environment For Automated Reasoning About Partial Functions. | David A. Basin |
| 1988 | Type Inference in Prolog. | H. Azzoune |
| 1988 | The TPS Theorem Proving System. | Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning |
| 1988 | PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. | P. E. Allen, Soumitra Bose, Edmund M. Clarke, Spiro Michaylov |
| 1988 | Propositional Temporal Interval Logic is PSPACE Complete. | A. A. Aaby, K. T. Narayana |
| 1986 | Negative Paramodulation. | Larry Wos, William McCune |
| 1986 | Diamond Formulas in the Dynamic Logic of Recursively Enumerable Programs. | Volker Weispfenning |
| 1986 | SHD-Prover at University of Texas at Austin. | Tie-Cheng Wang |
| 1986 | ECR: An Equality Conditional Resolution Proof Procedure. | Tie-Cheng Wang |
| 1986 | A Classification of Many-Sorted Unification Problems. | Christoph Walther |
| 1986 | Deductive Synthesis of Sorting Programs. | Jonathan Traugott |
| 1986 | Nested Resolution. | Jonathan Traugott |
| 1986 | How to Prove Equivalence of Term Rewriting Systems without Induction. | Yoshihito Toyama |
| 1986 | Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols. | Erik Tidn |
| 1986 | The KRIPKE Automated Theorem Proving System. | Paul B. Thistlewaite, Michael A. McRobbie, Robert K. Meyer |
| 1986 | The KLAUS Automated Deduction System. | Mark E. Stickel |
| 1986 | A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. | Mark E. Stickel |
| 1986 | An Improvement of Deduction Plans: Refutation Plans. | Hans-Albert Schneider |
| 1986 | Computational Aspects of Three-Valued Logic. | Peter H. Schmitt |
| 1986 | Unification in Many-Sorted Eqational Theories. | Manfred Schmidt-Schau |
| 1986 | Full-Commutation and Fair-Termination in Equational (and Combined) Term-Rewriting Systems. | Sara Porat, Nissim Francez |
| 1986 | Abstraction Using Generalization Functions. | David A. Plaisted |
| 1986 | A Simple Non-Termination Test for the Knuth-Bendix Method. | David A. Plaisted |