Canonical Equational Proofs

Bachmair (Autor)

Buch | Softcover

138 Seiten

1991 | Softcover reprint of the original 1st ed. 1991
Birkhauser Boston Inc (Verlag)
978-0-8176-3555-8 (ISBN)

Artikel merken

Equations occur in many computer applications, such as symbolic compu tation, functional programming, abstract data type specifications, program verification, program synthesis, and automated theorem proving. Rewrite systems are directed equations used to compute by replacing subterms in a given formula by equal terms until a simplest form possible, called a normal form, is obtained. The theory of rewriting is concerned with the compu tation of normal forms. We shall study the use of rewrite techniques for reasoning about equations. Reasoning about equations may, for instance, involve deciding whether an equation is a logical consequence of a given set of equational axioms. Convergent rewrite systems are those for which the rewriting process de fines unique normal forms. They can be thought of as non-deterministic functional programs and provide reasonably efficient decision procedures for the underlying equational theories. The Knuth-Bendix completion method provides a means of testing for convergence and can often be used to con struct convergent rewrite systems from non-convergent ones. We develop a proof-theoretic framework for studying completion and related rewrite based proof procedures. We shall view theorem provers as proof transformation procedures, so as to express their essential properties as proof normalization theorems.

1 Equational Proofs.- 1.1. Introduction.- 1.2. Terms.- 1.3. Equations.- 1.4. Orderings.- 1.5. Proofs.- 2 Standard Completion.- 2.1. Basic Completion.- 2.2. Proof Transformation.- 2.3. Proof Simplification.- 2.4. Fairness and Correctness.- 2.5. Standard Completion.- 2.6. Critical Pair Criteria.- 3 Extended Completion.- 3.1. Rewriting Modulo a Congruence.- 3.2. The Left-Linear Rule Method.- 3.3. Church-Rosser Systems.- 3.4. Extended Completion.- 3.5. The Extended Rule Method.- 3.6. Associative-Commutative Completion.- 3.7. The Protected Rule Method.- 3.8. Extended Critical Pair Criteria.- 4 Ordered Completion.- 4.1. Ordered Completion.- 4.2. Construction of Convergent Rewrite Systems.- 4.3. Refutational Theorem Proving.- 4.4. Horn Clauses with Equality.- 5 Proof by Consistency.- 5.1. Consistency and Ground Reducibility.- 5.2. Proof by Consistency.- 5.3. Refutation Completeness.- 5.4. Covering Sets.

Erscheint lt. Verlag	1.6.1991
Reihe/Serie	Progress in Theoretical Computer Science
Zusatzinfo	X, 138 p.
Verlagsort	Secaucus
Sprache	englisch
Maße	155 x 235 mm
Themenwelt	Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre
ISBN-10	0-8176-3555-6 / 0817635556
ISBN-13	978-0-8176-3555-8 / 9780817635558
Zustand	Neuware