| 1986 | TRSPEC: A Term Rewriting Based System for Algebraic Specifications. | Jrgen Avenhaus, Benjamin Benninghofen, Rdiger Gbel, Klaus Madlener |
| 1986 | The TPS Theorem Proving System. | Peter B. Andrews, Frank Pfenning, Sunil Issar, Carl P. Klapper |
| 1986 | Connections and Higher-Order Logic. | Peter B. Andrews |
| 1986 | Modal Theorem Proving. | Martn Abadi, Zohar Manna |
| 1984 | The Linked Inference Principle, II: The User's Viewpoint. | Larry Wos, Robert Veroff, Barry Smith, William McCune |
| 1984 | A Linear Characterization of NP-Complete Problems. | Silvio Ursic |
| 1984 | The Next Generation of Interactive Theorem Provers. | Patrick Suppes |
| 1984 | A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity. | Mark E. Stickel |
| 1984 | A Linear Time Algorithm for a Subcase of Second Order Instantiation. | Donald Simon |
| 1984 | Universal Unification. | Jrg H. Siekmann |
| 1984 | A Programming Notation for Tactical Reasoning. | David A. Schmidt |
| 1984 | Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving. | David A. Plaisted |
| 1984 | Analytic and Non-analytic Proofs. | Frank Pfenning |
| 1984 | Solving Word Problems in Free Algebras Using Complexity Functions. | Alex Pelin, Jean H. Gallier |
| 1984 | A New Interpretation of the Resolution Principle. | Etienne Paul |
| 1984 | Solving a Problem in Relevance Logic with an Automated Theorem Prover. | Hans Jrgen Ohlbach, Graham Wrightson |
| 1984 | The Mechanization of Existence Proofs of Recursive Predicates. | Ketan Mulmuley |
| 1984 | Applications of Protected Circumscription. | Jack Minker, Donald Perlis |
| 1984 | Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. | Dale Miller |
| 1984 | A Portable Environment for Research in Automated Reasoning. | Ewing L. Lusk, Ross A. Overbeek |
| 1984 | Term Rewriting Systems and Algebra. | Pierre Lescanne |
| 1984 | A Progress Report on New Decision Algorithms for Finitely Prsented Abelian Groups. | Dallas Lankford, Gregory Butler II, A. M. Ballantyne |
| 1984 | A General Inductive Completion Algorithm and Application to Abstract Data Types. | Hlne Kirchner |
| 1984 | A New Equational Unification Method: A Generalization of Martelli-Montanari's Algorithm. | Claude Kirchner |
| 1984 | EKL - A Mathematically Oriented Proof Checker. | Jussi Ketonen |