Wolfgang (Hrsg.) Bibel
5th Conference on Automated Deduction
Les Arcs, France, July 8-11, 1980
Buch
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 const…
Mehr
Beschreibung
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.
CHF 108.00
Preise inkl. MwSt. und Versandkosten (Portofrei ab CHF 40.00)
V103:
Folgt in ca. 5 Arbeitstagen
Produktdetails
Weitere Autoren: Kowalski, R. (Hrsg.)
- ISBN: 978-3-540-10009-6
- EAN: 9783540100096
- Produktnummer: 3242137
- Verlag: Springer Berlin Heidelberg
- Sprache: Englisch
- Erscheinungsjahr: 1980
- Seitenangabe: 404 S.
- Masse: H23.5 cm x B15.5 cm x D2.1 cm 610 g
- Auflage: 1980
- Abbildungen: Paperback
- Gewicht: 610
17 weitere Werke von Wolfgang (Hrsg.) Bibel:
Les Arcs, France, July 8-11, 1980
Ebook (PDF Format)
CHF 46.00
Les Arcs, France, July 8-11, 1980
Ebook (PDF Format)
CHF 106.50
Les Arcs, France, July 8-11, 1980
Ebook (PDF Format)
CHF 50.00
Bewertungen
0 von 0 Bewertungen
Anmelden
Keine Bewertungen gefunden. Seien Sie der Erste und teilen Sie Ihre Erkenntnisse mit anderen.