A Taste of Rewrite Systems

Abstract. This survey of the theory and applications of rewriting with equations discusses the existence and uniqueness of normal forms, the Knuth-Bendix completion procedure and its variations, as well as rewriting-based functional and logic programming and equational, rst-order, and inductive theorem proving. Ordinary, associative-commutative, and conditional rewriting are covered. Current areas of research are summarized and an extensive bibliography is provided. 0 Menu Equational reasoning is an important component in symbolic algebra, automated deduction, high-level programming languages, program veri cation, and arti cial intelligence. Reasoning with equations involves deriving consequences of given equations and nding values for variables that satisfy a given equation. Rewriting is avery powerful methodfor dealing with equations. Directed equations, called rewrite rules", are used to replace equals by equals, but only in the indicated direction. The theory of rewriting ...

• Type: Conference
• Year: 1993
• Where: MCMASTER
• Authors: Nachum Dershowitz
• Keywords: Automated Deduction, Conditional Rewriting, MCMASTER 1993, Normal Forms, Programming Languages