Canonical inference

An abstract proof-theoretic framework, inspired by rewriting methods, is proposed. Normal-form proof objects are minimal in some wellfounded proof ordering. The approach applies in the equational, Hornclause, and deduction-modulo cases, among others, as they incorporate formal notions of simplification and redundancy.