Publications

Canonical inference for implicational systems  (2008)

Authors:
Maria Paola Bonacina; Nachum Dershowitz
Title:
Canonical inference for implicational systems
Year:
2008
Type of item:
Contributo in atti di convegno
Tipologia ANVUR:
Contributo in Atti di convegno
Language:
Inglese
Format:
A Stampa
Name of journal:
Lecture Notes in Artificial Intelligence
N° Volume:
5195
Congresso:
Fourth International Joint Conference on Automated Reasoning (IJCAR)
Place:
Sydney, Australia
Period:
August 2008
:
Springer
Publisher:
Springer
ISBN:
9783540710691
Page numbers:
380-395
Short description of contents:
Completion is a general paradigm for applying inferences to generate a canonical presentation of a logical theory, or to semi-decide the validity of theorems, or to answer queries. We investigate what canonicity means for implicational systems that are axiomatizations of Moore families - or, equivalently, of propositional Horn theories. We build a correspondence between implicational systems and associative-commutative rewrite systems, give deduction mechanisms for both, and show how their respective inferences correspond. Thus, we exhibit completion procedures designed to generate canonical systems that are ``optimal'' for forward chaining, to compute minimal models, and to generate canonical systems that are rewrite-optimal. Rewrite-optimality is a new notion of ``optimality'' for implicational systems, one that takes contraction by simplification into account.
Web page:
http://dx.doi.org/10.1007/978-3-540-71070-7_33; http://profs.sci.univr.it/~bonacina/
Product ID:
46049
Handle IRIS:
11562/316091
Deposited On:
September 2, 2008
Last Modified:
August 28, 2017
Bibliographic citation:
Maria Paola Bonacina; Nachum Dershowitz, Canonical inference for implicational systems in «Lecture Notes in Artificial Intelligence» vol. 5195 Springer  in Proceedings of the Fourth International Joint Conference on Automated ReasoningSpringerProceedings of "Fourth International Joint Conference on Automated Reasoning (IJCAR)" , Sydney, Australia , August 2008 , 2008pp. 380-395

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
<<back

Activities

Research facilities