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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.