5th Conference on Automated Deduction
Les Arcs, France, July 8-11, 1980
(Sprache: Englisch)
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...
Leider schon ausverkauft
versandkostenfrei
Buch
80.24 €
Produktdetails
Produktinformationen zu „5th Conference on Automated Deduction “
Klappentext zu „5th Conference on Automated Deduction “
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.
Inhaltsverzeichnis zu „5th Conference on Automated Deduction “
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.
Autoren-Porträt
Prof. Dr. Wolfgang Bibel lehrt das Fachgebiet Intellektik am Fachbereich Informatik der TH Darmstadt.
Bibliographische Angaben
- 1980, 1980, 388 Seiten, Maße: 15,5 x 23,5 cm, Kartoniert (TB), Englisch
- Ed. by Wolfgang Bibel and R. Kowalski
- Herausgegeben: R. Kowalski, Wolfgang Bibel
- Verlag: Springer
- ISBN-10: 3540100091
- ISBN-13: 9783540100096
- Erscheinungsdatum: 01.06.1980
Sprache:
Englisch
Kommentar zu "5th Conference on Automated Deduction"
0 Gebrauchte Artikel zu „5th Conference on Automated Deduction“
Zustand | Preis | Porto | Zahlung | Verkäufer | Rating |
---|
Schreiben Sie einen Kommentar zu "5th Conference on Automated Deduction".
Kommentar verfassen