| 1984 | 7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings Robert E. Shostak |
| 1984 | A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity. Mark E. Stickel |
| 1984 | A Decision Method for Linear Temporal Logic. Ana R. Cavalli, Luis Fariñas del Cerro |
| 1984 | A General Inductive Completion Algorithm and Application to Abstract Data Types. Hélène Kirchner |
| 1984 | A Linear Characterization of NP-Complete Problems. Silvio Ursic |
| 1984 | A Linear Time Algorithm for a Subcase of Second Order Instantiation. Donald Simon |
| 1984 | A Narrowing Procedure for Theories with Constructors. Laurent Fribourg |
| 1984 | A Natural Proof System Based on rewriting Techniques. Deepak Kapur, Balakrishnan Krishnamurthy |
| 1984 | A New Equational Unification Method: A Generalization of Martelli-Montanari's Algorithm. Claude Kirchner |
| 1984 | A New Interpretation of the Resolution Principle. Etienne Paul |
| 1984 | A Portable Environment for Research in Automated Reasoning. Ewing L. Lusk, Ross A. Overbeek |
| 1984 | A Programming Notation for Tactical Reasoning. David A. Schmidt |
| 1984 | A Progress Report on New Decision Algorithms for Finitely Prsented Abelian Groups. Dallas Lankford, Gregory Butler II, A. M. Ballantyne |
| 1984 | A Satisfiability Tester for Non-Clausal Propositional Calculus. Allen Van Gelder |
| 1984 | Analytic and Non-analytic Proofs. Frank Pfenning |
| 1984 | Applications of Protected Circumscription. Jack Minker, Donald Perlis |
| 1984 | Associative-Commutative Unification. François Fages |
| 1984 | Canonical Forms in Finitely Presented Algebras. Philippe le Chenadec |
| 1984 | EKL - A Mathematically Oriented Proof Checker. Jussi Ketonen |
| 1984 | Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. Dale Miller |
| 1984 | Implementation Strategies for Plan-Based Deduction. Kenneth Forsythe, Stan Matwin |
| 1984 | Solving Word Problems in Free Algebras Using Complexity Functions. Alex Pelin, Jean H. Gallier |
| 1984 | Solving a Problem in Relevance Logic with an Automated Theorem Prover. Hans Jürgen Ohlbach, Graham Wrightson |
| 1984 | Term Rewriting Systems and Algebra. Pierre Lescanne |
| 1984 | Termination of a Set of Rules Modulo a Set of Equations. Jean-Pierre Jouannaud, Miguel Munoz |
| 1984 | The Linked Inference Principle, II: The User's Viewpoint. Larry Wos, Robert Veroff, Barry Smith, William McCune |
| 1984 | The Mechanization of Existence Proofs of Recursive Predicates. Ketan Mulmuley |
| 1984 | The Next Generation of Interactive Theorem Provers. Patrick Suppes |
| 1984 | Universal Unification. Jörg H. Siekmann |
| 1984 | Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving. David A. Plaisted |