Ground Canonicity
Nachum Dershowitz · arXiv (Cornell University) · 2003
We explore how different proof orderings induce different notions of saturation. We relate completion, paramodulation, saturation, redundancy elimination, and rewrite system reduction to proof orderings.