Completion for Rewriting Modulo a Congruence

We present completion methods for rewriting modulo a congruence, generalizing previous methods by Peterson and Stickel (1981) and Jouannaud and Kirchner (1986). We formalize our methods as equational inference systems and describe techniques for reasoning about such systems.

• Type: Conference
• Year: 1987
• Where: RTA
• Authors: Leo Bachmair, Nachum Dershowitz
• Keywords: Completion Methods, Equational Inference Systems, Generalizing, RTA 1987, Theoretical Computer Science