Term Rewriting Systems: From Church-Rosser to Knuth-Bendix and Beyond

Termrewritingsystemsare importantfor computabilitytheoryof abstractdata types,for automatictheorem proving, and for the foundationsof functionalprogramming.In this shortsurveywe present,starting from first principles,severalof the basic notions and facts in the area of term rewriting.Our treatment, whichoften will be informal,coversabstractrewriting,CombinatoryLogic, orthogonalsystems,strategies,criticalpair completion,and someextendedrewritingformats. Note: Researchpartiallysupportedby ESPRITprojects3020:Integrationand 3074:Semagraph.

• Type: Conference
• Year: 1990
• Where: ICALP
• Authors: Jan Willem Klop
• Keywords: Abstractdata Types, For Automatictheorem, ICALP 1990, Programming Languages, Termrewritingsystemsare Importantfor Computabilitytheoryof