Abstract canonical inference
Maria Paola Bonacina, Nachum Dershowitz · 2007
Abstract. This paper applies an abstract framework of canonical inference to explore how different proof orderings induce different variations of saturation and completeness. It defines fairness in terms of proof orderings, distinguishing between “fairness, ” which yields completeness, and “uniform fairness, ” which yields saturation. Notions like completion, paramodulation, saturation, redundancy elimination, and rewrite-system reduction are connected to proof orderings.