Abstract Canonical Inference: 
On Fairness in Theorem Proving

Maria Paola Bonacina and Nachum Dershowitz

SVARM
June 2012

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.