Publications

Authors:

Bonacina, Maria Paola; Nachum, Dershowitz

Title:

Canonical inference for implicational systems

Year:

2008

Type of item:

Contributo in volume (Capitolo o Saggio)

Tipologia ANVUR:

Contributo in volume (Capitolo o Saggio)

Language:

Inglese

Format:

A Stampa

Book Title:

Automated Reasoning - 4th International Joint Conference, IJCAR 2008 - Sydney, Australia, August 2008, Proceedings

Publisher:

Springer

ISBN:

9783540710691

Page numbers:

380-395

Keyword:

Automated reasoning; Knowledge compilation; Horn theories

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
https://mariapaola.github.io/

Product ID:

114330

Handle IRIS:

11562/316091

Deposited On:

September 2, 2008

Last Modified:

September 16, 2023

Bibliographic citation:

Bonacina, Maria Paola; Nachum, Dershowitz, Canonical inference for implicational systems Automated Reasoning - 4th International Joint Conference, IJCAR 2008 - Sydney, Australia, August 2008, Proceedings , 2008 , Springer , 2008 , pp. 380-395

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