| 1980 | 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings Wolfgang Bibel, Robert A. Kowalski |
| 1980 | A Complete, Nonredundant Algorithm for Reversed Skolemization. Philip T. Cox, Tomasz Pietrzykowski |
| 1980 | A Note on Resolution: How to Get Rid of Factoring without Loosing Completeness. Helga Noll |
| 1980 | A System for Proving Equivalences of Recursive Programs. Laurent Kott |
| 1980 | Abstraction Mappings in Mechanical Theorem Proving. David A. Plaisted |
| 1980 | Adding Dynamic Paramodulation to Rewrite Algorithms. Paul Y. Gloess, Jean-Pierre H. Laurent |
| 1980 | An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus. Rob Nederpelt |
| 1980 | An Experiment with "Edinburgh LCF". Jacek Leszczylowski |
| 1980 | An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions. Paul Y. Gloess |
| 1980 | Analysis of Dependencies to Improve the Behaviour of Logic Programs. Maurice Bruynooghe |
| 1980 | Canonical Forms and Unification. Jean-Marie Hullot |
| 1980 | Data Structures and Control Architectures for Implementation of Theorem-Proving Programs. Ross A. Overbeek, Ewing L. Lusk |
| 1980 | Deciding Unique Termination of Permutative Rewriting Systems: Choose Your Term Algebra Carefully. Hans-Josef Jeanrond |
| 1980 | Decision Procedures for Some Fragments of Set Theory. Alfredo Ferro, Eugenio G. Omodeo, Jacob T. Schwartz |
| 1980 | Generating Contours of Integration: An Application of Prolog in Symbolic Computing. Gábor Belovári, John A. Campbell |
| 1980 | How to Prove Algebraic Inductive Hypotheses Without Induction. Joseph A. Goguen |
| 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 | Program Synthesis from Incomplete Specifiactions. Gérard D. Guiho, Christian Gresse |
| 1980 | Proofs as Description of Computation. Chris Goad |
| 1980 | Reasoning by Plausible Inference. Leonard Friedman |
| 1980 | Selective Backtracking for Logic Programs. Luís Moniz Pereira, António Porto |
| 1980 | Simplifying Interpreted Formulas. Donald W. Loveland, Robert E. Shostak |
| 1980 | Specification and Verification of Real-Time, Distributed Systems Using the Theory of Constraints. Frederick C. Furtek |
| 1980 | The AFFIRM Theorem Prover: Proof Forests and Management of Large Proofs. Roddy W. Erickson, David R. Musser |
| 1980 | Transforming Matings into Natural Deduction Proofs. Peter B. Andrews |
| 1980 | Using Meta-Level Inference for Selective Application of Multiple Rewrite Rules in Algebraic Manipulation. Alan Bundy, Bob Welham |
| 1980 | Using Meta-Theoretic Reasoning to do Algebra. Luigia Carlucci Aiello, Richard W. Weyhrauch |
| 1980 | Variable Elimination and Chaining in a Resolution-based Prover for Inequalities. W. W. Bledsoe, Larry M. Hines |