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:

Nachum Dershowitz and Claude Kirchner. Abstract canonical presentations. Theoretical Computer Science 357:53-69, 2006 (presented in part at LICS 2003)

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:

Maria Paola Bonacina and Nachum Dershowitz. Abstract canonical inference. ACM Transactions on Computational Logic 8(1):180-208, January 2007 (presented in part at FTP 2003).

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.) In Memory of Harald Ganzinger. Springer, Lecture Notes in Artificial Intelligence, 1-36, to appear, accepted February 2011.

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 Fourth International Joint Conference on Automated Reasoning (IJCAR), Sydney, Australia, August 2008. LNAI 5195, 380-395, Springer 2008,

giving completion procedures to generate "optimal" implicational systems according to various notions, and with connections to my early work on rewrite programs.

Related works:

Guillaume Burel and Claude Kirchner. Regaining cut admissibility in deduction modulo using abstract completion. Information and Computation 208(2):140-164, 2010 (presented in part at LICS 2006).
Guillaume Burel and Claude Kirchner. Completion is an instance of abstract canonical system inference. In Kokichi Futatsugi, Jean-Pierre Jouannaud and José Meseguer (Eds.) Algebra, Meaning and Computation - Essays in Honor of Joseph Goguen, LNCS 4060, 497-520, Springer 2006.

Maria Paola Bonacina