Abstract Canonical Inference

TL;DR

This paper introduces an abstract framework for canonical inference, analyzing how proof orderings influence saturation and completeness, and clarifies the concepts of fairness in deductive mechanisms.

Contribution

It provides a unified theoretical approach connecting proof orderings with various inference procedures and fairness notions in logical deduction.

Findings

Different proof orderings lead to distinct saturation and completeness variants.

Fairness concepts are formalized, distinguishing between fairness and uniform fairness.

The framework unifies multiple inference concepts under a common abstract theory.

Abstract

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.