Canonicity of presentations, inferences and proofs

Starting from a study of presentations of theories and their properties (complete, saturated, contracted, canonical - i.e., saturated and contracted - reduced and perfect - i.e., complete and reduced) in an abstract framework based on well-founded orderings on proofs: we investigated properties of derivations (fair, uniformly fair), that produce such presentations, in completion procedures for saturation and proof procedures for refutation, via superposition/paramodulation, redundancy elimination and rewrite system reduction: We extended this framework from equational to Horn theories: including canonicity of implicational systems, that are presentations of Moore families, or, equivalently, of propositional Horn theories: giving completion procedures to generate "optimal" implicational systems according to various notions, and with connections to my early work on rewrite programs.

Related works:

Maria Paola Bonacina