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:

Maria Paola Bonacina and Nachum Dershowitz. Abstract canonical inference. ACM Transactions on Computational Logic 8(1):180-208, January 2007; DOI: 10.1145/1182613.1182619 (archived in CoRR as arXiv:cs/0406030v2; presented at FTP 2003 and at SVARM+VERIFY 2012).

We extended this framework from equational to Horn theories:

Maria Paola Bonacina and Nachum Dershowitz. Canonical ground Horn theories. In Andrei Voronkov and Christoph Weidenbach (Eds.) Programming Logics: Essays in Memory of Harald Ganzinger. Springer, Lecture Notes in Artificial Intelligence 7797, 35-71, March 2013 (invited); DOI: 10.1007/978-3-642-37651-1_3.

including canonicity of implicational systems, that are presentations of Moore families, or, equivalently, of propositional Horn theories:

Maria Paola Bonacina and Nachum Dershowitz. Canonical inference for implicational systems. In Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR), Sydney, Australia, August 2008. Springer, Lecture Notes in Artificial Intelligence 5195, 380-395, 2008; DOI: 10.1007/978-3-540-71070-7_33,

While working on these topics I also co-authored a survey:

Maria Paola Bonacina and Alberto Martelli. Automated Reasoning. Intelligenza Artificiale, 3(1-2):14-20 (Special issue on Artificial Intelligence 50th Anniversary 1956-2006) June 2006 (invited).

Maria Paola Bonacina