This page in English
SucheAbstract Abstract Reduction
G. Struth
erschienen 2006
in B. Möller (ed.)
Journal of Logic and Algebraic Programming 66
Special issue "Relation Algebra and Kleene Algebra", pp. 239-270
We propose novel algebraic proof techniques for rewrite systems. Church-Rosser theorems and further fundamental statements that do not mention termination are proved in Kleene algebra. Certain reduction and transformation theorems for termination that depend on abstract commutation, cooperation or simulation properties are proved in an extension with infinite iteration. Benefits of the algebraic approach are simple concise calculational proofs by equational reasoning, connection with automata-based decision procedures and a natural formal semantics for rewriting diagrams. It is therefore especially suited for mechanization and automation.
Special issue "Relation Algebra and Kleene Algebra", pp. 239-270
We propose novel algebraic proof techniques for rewrite systems. Church-Rosser theorems and further fundamental statements that do not mention termination are proved in Kleene algebra. Certain reduction and transformation theorems for termination that depend on abstract commutation, cooperation or simulation properties are proved in an extension with infinite iteration. Benefits of the algebraic approach are simple concise calculational proofs by equational reasoning, connection with automata-based decision procedures and a natural formal semantics for rewriting diagrams. It is therefore especially suited for mechanization and automation.