Publications

Canonical ground Horn theories  (2013)

Authors:
Maria Paola Bonacina; Nachum Dershowitz
Title:
Canonical ground Horn theories
Year:
2013
Type of item:
Contributo in volume (Capitolo o Saggio)
Tipologia ANVUR:
Contributo in volume (Capitolo o Saggio)
Nations of authors:
ISRAELE; ITALIA
Language:
Inglese
Format:
A Stampa
Book Title:
Programming Logics: Essays in memory of Harald Ganzinger
Publisher:
Springer
:
Heidelberg
ISBN:
9783642376504
Page numbers:
35-71
Keyword:
Horn theories, conditional theories, Moore families, decision procedures, canonical systems, normal forms, saturation, redundancy
Short description of contents:
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.
Web page:
http://profs.sci.univr.it/~bonacina/canonicity.html
Product ID:
59336
Handle IRIS:
11562/348366
Deposited On:
January 17, 2016
Last Modified:
November 2, 2016
Bibliographic citation:
Maria Paola Bonacina; Nachum Dershowitz, Canonical ground Horn theories Programming Logics: Essays in memory of Harald GanzingerHeidelbergSpringer2013pp. 35-71

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo IRIS

Related projects
Title Department Managers
Sintesi di procedure di decisione basate sulla deduzione con applicazioni all'analisi formale automatica di programmi (PRIN 2003) Department Informatica Maria Paola Bonacina
Integrazione di metodi di ragionamento automatico nel model checking: verifica formale automatica di sistemi di grande scala e a stati infiniti - Progetto ed integrazione di macchine di prova per l'analisi di programmi (PRIN 2007) Department Informatica Maria Paola Bonacina
<<back

Activities

Research facilities