Canonicity and fairness in deduction

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 the fairness properties of derivations producing such presentations in both completion procedures for saturation and proof procedures for refutation, that use 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, with connections to my work on rewrite programs. While working on these topics I also co-authored a brief survey: Related work on canonicity:

Maria Paola Bonacina