How to Prove Ground Confluence

Klaus Becker
Fachbereich Informatik
Universitaet Kaiserslautern
Postfach 3049
D-67653 Kaiserslautern 
Germany

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.

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1996/
file:Becker.SR-96-02.ps.gz