5th Conference on automated deduction : Les Arcs, France, July 8 11, 1980
Shranjeno v:
| Korporativna značnica: | |
|---|---|
| Drugi avtorji: | , |
| Format: | Livre numérique |
| Jezik: | Anglais |
| Izdano: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serija: | Lecture notes in computer science
87 |
| Teme: | |
| Online dostop: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Sporočilo: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, edited by W. Bibel and R. Kowalski, Berlin, Springer-Verlag, 1980, 1 vol. (VII-385 p.), Lecture notes in computer science, 0-387-10009-1 • 5th Conference on Automated Deduction, Texte imprimé, 9783662191958 |
Kazalo:
- 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.