Completion is the process of transforming a given set of equations into an equivalent confluent and terminating rewrite system. Rewriting is an attractive Turing-complete computational model based on directed equations. Rewrite systems that are confluent and terminating provide a simple decision procedure for validity problems in the underlying equational theory. Introduced 45 years ago by Knuth and Bendix, completion was heavily studied in the 1980s and 1990s. In this talk I give an introduction to completion, with a particular emphasis on recent findings concerning automation, correctness, presentation, and proof reconstruction.

Homepage Aart Middeldorp

Kaffee/Gebäck ab 13:45 im SR049, Takustr. 9