| 1986 | 8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings Jörg H. Siekmann |
| 1986 | A Classification of Many-Sorted Unification Problems. Christoph Walther |
| 1986 | A Commonsense Theory of Nonmonotonic Reasoning. Frank M. Brown |
| 1986 | A Geometry Theorem Prover Based on Buchberger's Algorithm. B. Kutzler, Sabine Stifter |
| 1986 | A New Formula for the Execution of Categorial Combinators. Rafael Dueire Lins |
| 1986 | A New Method for Establishing Refutational Completeness in Theorem Proving. Jieh Hsiang, Michaël Rusinowitch |
| 1986 | A Simple Non-Termination Test for the Knuth-Bendix Method. David A. Plaisted |
| 1986 | A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Mark E. Stickel |
| 1986 | AUTOLOGIC at University of Victoria. Charles G. Morgan |
| 1986 | Abstraction Using Generalization Functions. David A. Plaisted |
| 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 | An Improvement of Deduction Plans: Refutation Plans. Hans-Albert Schneider |
| 1986 | An Interactive Verification System Based on Dynamic Logic. Reiner Hähnle, Maritta Heisel, Wolfgang Reif, Werner Stephan |
| 1986 | Automatic Theorem Proving in the ISDV System. Christoph Beierle, Walter G. Olthoff, Angi Voß |
| 1986 | Causes for Events: Their Computation and Applications. Philip T. Cox, Tomasz Pietrzykowski |
| 1986 | Classes of First Order Formulas Under Various Satisfiability Definitions. Hans Kleine Büning, Theodor Lettmann |
| 1986 | Combination of Unification Algorithms. Alexander Herold |
| 1986 | Commutation, Transformation, and Termination. Leo Bachmair, Nachum Dershowitz |
| 1986 | Computational Aspects of Three-Valued Logic. Peter H. Schmitt |
| 1986 | Connections and Higher-Order Logic. Peter B. Andrews |
| 1986 | Controlling Deduction with Proof Condensation and Heuristics. Franz Oppacher, E. Suen |
| 1986 | Deductive Synthesis of Sorting Programs. Jonathan Traugott |
| 1986 | Diamond Formulas in the Dynamic Logic of Recursively Enumerable Programs. Volker Weispfenning |
| 1986 | ECR: An Equality Conditional Resolution Proof Procedure. Tie-Cheng Wang |
| 1986 | Formulation of Induction Formulas in Verification of Prolog Programs. Tadashi Kanamori, Hiroshi Fujita |
| 1986 | Full-Commutation and Fair-Termination in Equational (and Combined) Term-Rewriting Systems. Sara Porat, Nissim Francez |
| 1986 | GEO-Prover - A Geometry Theorem Prover Developed at UT. Shang-Ching Chou |
| 1986 | Highly Parallel Inference Machine. M. Bayerl |
| 1986 | How to Clear a Block: Plan Formation in Situational Logic. Zohar Manna, Richard J. Waldinger |
| 1986 | How to Prove Equivalence of Term Rewriting Systems without Induction. Yoshihito Toyama |
| 1986 | ITP at Argonne National Laboratory. Ewing L. Lusk, William McCune, Ross A. Overbeek |
| 1986 | Implementing Number Theory: An Experiment with Nuprl. Douglas J. Howe |
| 1986 | Matching with Distributivity. Jalel Mzali |
| 1986 | Mechanizing Constructive Proofs (Abstract). Gérard P. Huet |
| 1986 | Modal Theorem Proving. Martín Abadi, Zohar Manna |
| 1986 | NP-Completeness of the Set Unification and Matching Problems. Deepak Kapur, Paliath Narendran |
| 1986 | Negative Paramodulation. Larry Wos, William McCune |
| 1986 | Nested Resolution. Jonathan Traugott |
| 1986 | Overview of a Theorem-Prover for A Computational Logic. Robert S. Boyer, J Strother Moore |
| 1986 | Parallel Algorithms for Term Matching. Cynthia Dwork, Paris C. Kanellakis, Larry J. Stockmeyer |
| 1986 | Parallel Theorem Proving with Connection Graphs. Rasiah Loganantharaj, Robert A. Mueller |
| 1986 | Paths to High-Performance Automated Theorem Proving. Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek |
| 1986 | Program Verifier "Tatzelwurm": Reasoning about Systems of Linear Inequalities. Thomas Käufl |
| 1986 | Proof by Induction Using Test Sets. Deepak Kapur, Paliath Narendran, Hantao Zhang |
| 1986 | Proving Termination of Associative Commutative Rewriting Systems by Rewriting. Isabelle Gnaedig, Pierre Lescanne |
| 1986 | Purely Functional Implementation of a Logic. F. Keith Hanna, Neil Daeche |
| 1986 | REVE a Rewrite Rule Laboratory. Pierre Lescanne |
| 1986 | RRL: A Rewrite Rule Laboratory. Deepak Kapur, G. Sivakumar, Hantao Zhang |
| 1986 | Relating Resolution and Algebraic Completion for Horn Logic. Roland Dietrich |
| 1986 | Resolution and Quantified Epistemic Logics. Kurt Konolige |
| 1986 | SHD-Prover at University of Texas at Austin. Tie-Cheng Wang |
| 1986 | Some Contributions to the Logical Analysis of Circumscrition. Gerhard Jäger |
| 1986 | Some Relationships between Unification, restricted Unification, and Matching. Hans-Jürgen Bürckert |
| 1986 | Sufficient Completness, Term Rewriting Systems and "Anti-Unification". Hubert Comon |
| 1986 | THINKER. Francis Jeffry Pelletier |
| 1986 | TRSPEC: A Term Rewriting Based System for Algebraic Specifications. Jürgen Avenhaus, Benjamin Benninghofen, Rüdiger Göbel, Klaus Madlener |
| 1986 | The Heuristics and Experimental Results of a New Hyperparamodulation: HL-Resolution. Younghwan Lim |
| 1986 | The Illinois Prover: A General Purpose Resolution Theorem Prover. Steven Greenbaum, David A. Plaisted |
| 1986 | The J-Machine: Functional Programming with Combinators. Jacek Gibert |
| 1986 | The KLAUS Automated Deduction System. Mark E. Stickel |
| 1986 | The KRIPKE Automated Theorem Proving System. Paul B. Thistlewaite, Michael A. McRobbie, Robert K. Meyer |
| 1986 | The Karlsruhe Induction Theorem Proving System. Susanne Biundo, Birgit Hummel, Dieter Hutter, Christoph Walther |
| 1986 | The Markgraf Karl Refutation Procedure (MKRP). Norbert Eisinger, Hans Jürgen Ohlbach |
| 1986 | The Passau RAP System: Prototyping Algebraic Specifications Using Conditional Narrowing. Heinrich Hußmann |
| 1986 | The TPS Theorem Proving System. Peter B. Andrews, Frank Pfenning, Sunil Issar, Carl P. Klapper |
| 1986 | Theorem Proving Systems of the Formel Project. Gérard P. Huet |
| 1986 | Theory Links in Semantic Graphs. Neil V. Murray, Erik Rosenthal |
| 1986 | Unification in Boolean Rings. Ursula Martin, Tobias Nipkow |
| 1986 | Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols. Erik Tidén |
| 1986 | Unification in Many-Sorted Eqational Theories. Manfred Schmidt-Schauß |
| 1986 | Unification in the Data Structure Sets. Wolfram Büttner |
| 1986 | Using Narrowing to do Isolation in Symbolic Equation Solving - An Experiment in Automated Reasoning. A. J. J. Dick, Jim Cunningham |
| 1986 | What You Always Wanted to Know About Clause Graph Resolution. Norbert Eisinger |