E-Books durchsuchen

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

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