How to Prove Ground Confluence
Becker, Klaus · 1996
We show how to prove ground confluence of term rewrite relations that are induced by reductive systems of clausal rewrite rules. According to a well-known critical pair criterion it suffices for such systems to prove ground joinability of a suitable set of `critical clauses'. We outline how the latter can be done in a systematic fashion, using mathematical induction as a key concept of reasoning. 1 Introduction and Motivation The notion of (ground) confluence is of great importance in the field of term rewriting: If the rewrite relation in focus is (ground) confluent, then one knows that term rewriting --- considered as a computation mechanism --- provides unique computation results. Note that the supplement "ground" is added if term rewriting is considered on ground terms (i.e. terms without variables) only. This restricted notion of confluence suffices in many applications/situations. Generally, ground confluence is easier to achieve than full confluence: There are rewrite syst...