Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01).
Nachum Dershowitz · Electronic Notes in Theoretical Computer Science · 2003
We explore how different proof orderings induce different notions of saturation and completeness. We relate completion, paramodulation, saturation, redundancy elimination, and rewrite system reduction to proof orderings.