An abstract framework of canonical inference is used to explore how different proof orderings induce different variants of saturation and completeness. Notions like completion, paramodulation, saturation, redundancy elimination, and rewrite-system reduction are connected to proof orderings. Fairness of deductive mechanisms is defined in terms of proof orderings, distinguishing between (ordinary) ``fairness,'' which yields completeness, and ``uniform fairness,'' which yields saturation.
|Titolo:||Abstract canonical inference|
|Data di pubblicazione:||2007|
|Appare nelle tipologie:||01.01 Articolo in Rivista|