Online Library TheLib.net » Canonical Equational Proofs
cover of the book Canonical Equational Proofs

Ebook: Canonical Equational Proofs

00
27.01.2024
0
0

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.








Content:
Front Matter....Pages i-x
Equational Proofs....Pages 1-11
Standard Completion....Pages 13-38
Extended Completion....Pages 39-71
Ordered Completion....Pages 73-98
Proof by Consistency....Pages 99-115
Back Matter....Pages 117-137



Content:
Front Matter....Pages i-x
Equational Proofs....Pages 1-11
Standard Completion....Pages 13-38
Extended Completion....Pages 39-71
Ordered Completion....Pages 73-98
Proof by Consistency....Pages 99-115
Back Matter....Pages 117-137
....
Download the book Canonical Equational Proofs for free or read online
Read Download
Continue reading on any device:
QR code
Last viewed books
Related books
Comments (0)
reload, if the code cannot be seen