5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980

Using meta-theoretic reasoning to do algebra....Pages 1-13
Generating contours of integration: An application of PROLOG in symbolic computing....Pages 14-23
Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation....Pages 24-38
Proofs as descriptions of computation....Pages 39-52
Program synthesis from incomplete specifications....Pages 53-62
A system for proving equivalences of recursive programs....Pages 63-69
Variable elimination and chaining in a resolution-based prover for inequalities....Pages 70-87
Decision procedures for some fragments of set theory....Pages 88-96
Simplifying interpreted formulas....Pages 97-109
Specification and verification of real-time, distributed systems using the theory of constraints....Pages 110-125
Reasoning by plausible inference....Pages 126-142
Logical support in a time-varying model....Pages 143-153
An experiment with the Boyer-Moore theorem prover: A proof of the correctness of a simple parser of expressions....Pages 154-169
An experiment with "Edinburgh LCF"....Pages 170-181
An approach to theorem proving on the basis of a typed lambda-calculus....Pages 182-194
Adding dynamic paramodulation to rewrite algorithms....Pages 195-207
Hyperparamodulation: A refinement of paramodulation....Pages 208-219
The AFFIRM theorem prover: Proof forests and management of large proofs....Pages 220-231
Data structures and control architecture for implementation of theorem-proving programs....Pages 232-249
A note on resolution: How to get rid of factoring without loosing completeness....Pages 250-263
Abstraction mappings in mechanical theorem proving....Pages 264-280
Transforming matings into natural deduction proofs....Pages 281-292
Analysis of dependencies to improve the behaviour of logic programs....Pages 293-305
Selective backtracking for logic programs....Pages 306-317
Canonical forms and unification....Pages 318-334
Deciding unique termination of permutative rewriting systems: Choose your term algebra carefully....Pages 335-355
How to prove algebraic inductive hypotheses without induction....Pages 356-373
A complete, nonredundant algorithm for reversed skolemization....Pages 374-385