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: 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: While working on these topics I also co-authored a survey:

Maria Paola Bonacina