| 1982 | Comparison of Natural Deduction and Locking Resolution Implementations. | Steven Greenbaum, A. Nagasaka, Paul O'Rorke, David A. Plaisted |
| 1982 | Automatic Construction of Special Purpose Programs. | Chris Goad |
| 1982 | Intuitonistic Basis for Non-Monotonic Logic. | Dov M. Gabbay |
| 1982 | Knowledge Retrieval as Limited Inference. | Alan M. Frisch, James F. Allen |
| 1982 | Proof by Matrix Reduction as Plan + Validation. | Ricardo Caferra |
| 1982 | The Power of the Church-Rosser Property for String Rewriting Systems. | Ronald V. Book |
| 1980 | Hyperparamodulation: A Refinement of Paramodulation. | Larry Wos, Ross A. Overbeek, Lawrence J. Henschen |
| 1980 | Logical Support in a Time-Varying Model. | Alan M. Thompson |
| 1980 | Abstraction Mappings in Mechanical Theorem Proving. | David A. Plaisted |
| 1980 | Selective Backtracking for Logic Programs. | Lus Moniz Pereira, Antnio Porto |
| 1980 | Data Structures and Control Architectures for Implementation of Theorem-Proving Programs. | Ross A. Overbeek, Ewing L. Lusk |
| 1980 | A Note on Resolution: How to Get Rid of Factoring without Loosing Completeness. | Helga Noll |
| 1980 | An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus. | Rob Nederpelt |
| 1980 | Simplifying Interpreted Formulas. | Donald W. Loveland, Robert E. Shostak |
| 1980 | An Experiment with "Edinburgh LCF". | Jacek Leszczylowski |
| 1980 | A System for Proving Equivalences of Recursive Programs. | Laurent Kott |
| 1980 | Deciding Unique Termination of Permutative Rewriting Systems: Choose Your Term Algebra Carefully. | Hans-Josef Jeanrond |
| 1980 | Canonical Forms and Unification. | Jean-Marie Hullot |
| 1980 | Program Synthesis from Incomplete Specifiactions. | Grard D. Guiho, Christian Gresse |
| 1980 | How to Prove Algebraic Inductive Hypotheses Without Induction. | Joseph A. Goguen |
| 1980 | Proofs as Description of Computation. | Chris Goad |
| 1980 | Adding Dynamic Paramodulation to Rewrite Algorithms. | Paul Y. Gloess, Jean-Pierre H. Laurent |
| 1980 | An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions. | Paul Y. Gloess |
| 1980 | Specification and Verification of Real-Time, Distributed Systems Using the Theory of Constraints. | Frederick C. Furtek |
| 1980 | Reasoning by Plausible Inference. | Leonard Friedman |