An abstract framework of canonical inference based on proof orderings is applied to ground Horn theories with equality. A finite presentation that makes all normal-form proofs available is called saturated. To maximize the chance that a saturated presentation be finite, it should also be contracted, in which case it is deemed canonical. We apply these notions to propositional Horn theorie - or equivalently Moore families - presented as implicational systems or associative-commutative rewrite systems, and ground equational Horn theories, presented as decreasing conditional rewrite systems. For implicational systems, we study different notions of optimality and the completion procedures that generate them, and we suggest a new notion of rewrite-optimality, that takes contraction by simplification into account. For conditional rewrite systems,we show that reduced (fully normalized) is stronger than contracted (sans redundancy), and accordingly the perfect system - complete and reduced - is preferred to the canonical one - saturated and contracted. We conclude with a survey of approaches to normal-form proofs, saturated, or canonical, systems, and decision procedures based on them.

Canonical ground Horn theories

BONACINA, Maria Paola
;
2013-01-01

Abstract

An abstract framework of canonical inference based on proof orderings is applied to ground Horn theories with equality. A finite presentation that makes all normal-form proofs available is called saturated. To maximize the chance that a saturated presentation be finite, it should also be contracted, in which case it is deemed canonical. We apply these notions to propositional Horn theorie - or equivalently Moore families - presented as implicational systems or associative-commutative rewrite systems, and ground equational Horn theories, presented as decreasing conditional rewrite systems. For implicational systems, we study different notions of optimality and the completion procedures that generate them, and we suggest a new notion of rewrite-optimality, that takes contraction by simplification into account. For conditional rewrite systems,we show that reduced (fully normalized) is stronger than contracted (sans redundancy), and accordingly the perfect system - complete and reduced - is preferred to the canonical one - saturated and contracted. We conclude with a survey of approaches to normal-form proofs, saturated, or canonical, systems, and decision procedures based on them.
2013
9783642376504
Horn theories; conditional theories; Moore families; decision procedures; canonical systems; normal forms; saturation; redundancy
File in questo prodotto:
File Dimensione Formato  
LNCS7797-2013HornCanonical.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 396.7 kB
Formato Adobe PDF
396.7 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/348366
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact