| 1986 | Combination of Unification Algorithms. | Alexander Herold |
| 1986 | Purely Functional Implementation of a Logic. | F. Keith Hanna, Neil Daeche |
| 1986 | An Interactive Verification System Based on Dynamic Logic. | Reiner Hhnle, Maritta Heisel, Wolfgang Reif, Werner Stephan |
| 1986 | The Illinois Prover: A General Purpose Resolution Theorem Prover. | Steven Greenbaum, David A. Plaisted |
| 1986 | Proving Termination of Associative Commutative Rewriting Systems by Rewriting. | Isabelle Gnaedig, Pierre Lescanne |
| 1986 | The J-Machine: Functional Programming with Combinators. | Jacek Gibert |
| 1986 | The Markgraf Karl Refutation Procedure (MKRP). | Norbert Eisinger, Hans Jrgen Ohlbach |
| 1986 | What You Always Wanted to Know About Clause Graph Resolution. | Norbert Eisinger |
| 1986 | Parallel Algorithms for Term Matching. | Cynthia Dwork, Paris C. Kanellakis, Larry J. Stockmeyer |
| 1986 | Relating Resolution and Algebraic Completion for Horn Logic. | Roland Dietrich |
| 1986 | Using Narrowing to do Isolation in Symbolic Equation Solving - An Experiment in Automated Reasoning. | A. J. J. Dick, Jim Cunningham |
| 1986 | Causes for Events: Their Computation and Applications. | Philip T. Cox, Tomasz Pietrzykowski |
| 1986 | Sufficient Completness, Term Rewriting Systems and "Anti-Unification". | Hubert Comon |
| 1986 | GEO-Prover - A Geometry Theorem Prover Developed at UT. | Shang-Ching Chou |
| 1986 | An Actual Implementation of a Procedure That Mechanically Proves Termination of Rewriting Systems Based on Inequalities Between Polynomial Interpretations. | Ahlem Ben Cherifa, Pierre Lescanne |
| 1986 | Unification in the Data Structure Sets. | Wolfram Bttner |
| 1986 | Paths to High-Performance Automated Theorem Proving. | Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek |
| 1986 | Some Relationships between Unification, restricted Unification, and Matching. | Hans-Jrgen Brckert |
| 1986 | Classes of First Order Formulas Under Various Satisfiability Definitions. | Hans Kleine Bning, Theodor Lettmann |
| 1986 | A Commonsense Theory of Nonmonotonic Reasoning. | Frank M. Brown |
| 1986 | Overview of a Theorem-Prover for A Computational Logic. | Robert S. Boyer, J Strother Moore |
| 1986 | The Karlsruhe Induction Theorem Proving System. | Susanne Biundo, Birgit Hummel, Dieter Hutter, Christoph Walther |
| 1986 | Automatic Theorem Proving in the ISDV System. | Christoph Beierle, Walter G. Olthoff, Angi Vo |
| 1986 | Highly Parallel Inference Machine. | M. Bayerl |
| 1986 | Commutation, Transformation, and Termination. | Leo Bachmair, Nachum Dershowitz |