Term rewriting systems: From Church-Rosser to Knuth-Bendix and beyond. (English) Zbl 0765.68008

Klop, Jan Willem

Automata, languages and programming, Proc. 17th Int. Colloq., Warwick/GB 1990, Lect. Notes Comput. Sci. 443, 350-369 (1990).

Summary: [For the entire collection see Zbl 0758.00017.]
Term rewriting systems are important for computationality theory of abstract data types, for automatic theorem proving, and for the foundations of functional programming. In this short survey we present, starting from first principles, several of the basic notions and facts in the area of terms rewriting. Our treatment, which often will be informal, covers abstract rewriting, combinatory logic, orthogonal systems, strategies, critical pair completion, and some extended rewriting formats.

MSC:

68-02	Research exposition (monographs, survey articles) pertaining to computer science
68Q42	Grammars and rewriting systems

Keywords:

Church-Rosser; repeated variables; Newman’s lemma; abstract reduction systems; Knuth-Bendix; equational logic; termination; narrowing; orthogonality; conditional rewriting; combinatory logic; critical pair completion

Citations:

Zbl 0758.00017

Software:

Miranda