| 1984 | A Natural Proof System Based on rewriting Techniques. | Deepak Kapur, Balakrishnan Krishnamurthy |
| 1984 | Termination of a Set of Rules Modulo a Set of Equations. | Jean-Pierre Jouannaud, Miguel Munoz |
| 1984 | A Satisfiability Tester for Non-Clausal Propositional Calculus. | Allen Van Gelder |
| 1984 | A Narrowing Procedure for Theories with Constructors. | Laurent Fribourg |
| 1984 | Implementation Strategies for Plan-Based Deduction. | Kenneth Forsythe, Stan Matwin |
| 1984 | Associative-Commutative Unification. | Franois Fages |
| 1984 | Canonical Forms in Finitely Presented Algebras. | Philippe le Chenadec |
| 1984 | A Decision Method for Linear Temporal Logic. | Ana R. Cavalli, Luis Farias del Cerro |
| 1982 | Solving Open Questions with an Automated Theorem-Proving Program. | Larry Wos |
| 1982 | Procedure Implementation Through Demodulation and Related Tricks. | Steven K. Winker, Larry Wos |
| 1982 | An Example of FOL Using Metatheory. | Richard W. Weyhrauch |
| 1982 | Meta-Level Inference and Program Verification. | Leon Sterling, Alan Bundy |
| 1982 | Derived Preconditions and Their Use in Program Synthesis. | Douglas R. Smith |
| 1982 | The Application of Homogenization to Simultaneous Equations. | Bernard Silver |
| 1982 | Universal Unification and a Classification of Equational Theories. | Jrg H. Siekmann, Peter Szab |
| 1982 | STP: A Mechanized Logic for Specification and Verification. | Robert E. Shostak, Richard L. Schwartz, P. M. Melliar-Smith |
| 1982 | Deciding Combinations of Theories. | Robert E. Shostak |
| 1982 | Exponential Improvement of Efficient Backtracking: A Strategy for Plan-Based Deduction. | Tomasz Pietrzykowski, Stan Matwin |
| 1982 | On Indefinite Databases and the Closed World Assumption. | Jack Minker |
| 1982 | A Look at TPS. | Dale A. Miller, Eve Longini Cohen, Peter B. Andrews |
| 1982 | Exponential Improvement of Efficient Backtracking: data Structure and Implementation. | Stan Matwin, Tomasz Pietrzykowski |
| 1982 | Logic Machine Architecture: Inference Mechanisms. | Ewing L. Lusk, William McCune, Ross A. Overbeek |
| 1982 | Logic Machine Architecture: Kernel Funtions. | Ewing L. Lusk, William McCune, Ross A. Overbeek |
| 1982 | Improvements of a Tautology-Testing Algorithm. | K. M. Hrnig, Wolfgang Bibel |
| 1982 | Representing Infinite Sequences of Resolvents in recursive First-Order Horn Databases. | Lawrence J. Henschen, Shamim A. Naqvi |