5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980 [electronic resource] / edited by Wolfgang Bibel, Robert Kowalski.

Using meta-theoretic reasoning to do algebra -- Generating contours of integration: An application of PROLOG in symbolic computing -- Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation -- Proofs as descriptions of computation -- Program synthesis from incomplete specifications -- A system for proving equivalences of recursive programs -- Variable elimination and chaining in a resolution-based prover for inequalities -- Decision procedures for some fragments of set theory -- Simplifying interpreted formulas -- Specification and verification of real-time, distributed systems using the theory of constraints -- Reasoning by plausible inference -- Logical support in a time-varying model -- An experiment with the Boyer-Moore theorem prover: A proof of the correctness of a simple parser of expressions -- An experiment with "Edinburgh LCF" -- An approach to theorem proving on the basis of a typed lambda-calculus -- Adding dynamic paramodulation to rewrite algorithms -- Hyperparamodulation: A refinement of paramodulation -- The AFFIRM theorem prover: Proof forests and management of large proofs -- Data structures and control architecture for implementation of theorem-proving programs -- A note on resolution: How to get rid of factoring without loosing completeness -- Abstraction mappings in mechanical theorem proving -- Transforming matings into natural deduction proofs -- Analysis of dependencies to improve the behaviour of logic programs -- Selective backtracking for logic programs -- Canonical forms and unification -- Deciding unique termination of permutative rewriting systems: Choose your term algebra carefully -- How to prove algebraic inductive hypotheses without induction -- A complete, nonredundant algorithm for reversed skolemization.