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