How to Prove Ground Confluence

Abstract

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.