A tableau calculus for a nonmonotonic extension of ℰℒ ⊥

Laura Giordano; Valentina Gliozzi; Nicola Olivetti; Gian Luca Pozzato

doi:10.1007/978-3-642-22119-4_15

A tableau calculus for a nonmonotonic extension of ℰℒ ^⊥

Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato

Dipartimento di Scienze e Innovazione Tecnologica

Risultato della ricerca: Capitolo in libro/report/atti di convegno › Contributo a conferenza › peer review

Abstract

We introduce a tableau calculus for a nonmonotonic extension of low complexity Description Logic ℰℒ^⊥ that can be used to reason about typicality and defeasible properties. The calculus deals with Left Local knowledge bases in the logic ℰℒ^⊥T_min recently introduced in [8]. The calculus performs a two-phase computation to check whether a query is minimally entailed from the initial knowledge base. It is sound, complete and terminating. Furthermore, it is a decision procedure for Left Local ℰℒ^⊥T_min knowledge bases, whose complexity matches the known results for the logic, namely that entailment is in Π₂^p.

Lingua originale	Inglese
Titolo della pubblicazione ospite	Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings
Pagine	180-195
Numero di pagine	16
DOI	https://doi.org/10.1007/978-3-642-22119-4_15
Stato di pubblicazione	Pubblicato - 2011
Evento	20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011 - Bern, Switzerland Durata: 4 lug 2011 → 8 lug 2011

Serie di pubblicazioni

Nome	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6793 LNAI
ISSN (stampa)	0302-9743
ISSN (elettronico)	1611-3349

???event.eventtypes.event.conference???

???event.eventtypes.event.conference???	20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011
Paese/Territorio	Switzerland
Città	Bern
Periodo	4/07/11 → 8/07/11

Accesso al documento

10.1007/978-3-642-22119-4_15

Altri file e collegamenti

Link to publication in Scopus

Cita questo

Giordano, L., Gliozzi, V., Olivetti, N., & Pozzato, G. L. (2011). A tableau calculus for a nonmonotonic extension of ℰℒ ^⊥. In Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings (pagg. 180-195). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6793 LNAI). https://doi.org/10.1007/978-3-642-22119-4_15

Giordano, Laura ; Gliozzi, Valentina ; Olivetti, Nicola et al. / A tableau calculus for a nonmonotonic extension of ℰℒ ^⊥. Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. 2011. pagg. 180-195 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e55532430f3b41739c0226e4a54184ff,

title = "A tableau calculus for a nonmonotonic extension of ℰℒ ⊥",

abstract = "We introduce a tableau calculus for a nonmonotonic extension of low complexity Description Logic ℰℒ⊥ that can be used to reason about typicality and defeasible properties. The calculus deals with Left Local knowledge bases in the logic ℰℒ⊥Tmin recently introduced in [8]. The calculus performs a two-phase computation to check whether a query is minimally entailed from the initial knowledge base. It is sound, complete and terminating. Furthermore, it is a decision procedure for Left Local ℰℒ⊥Tmin knowledge bases, whose complexity matches the known results for the logic, namely that entailment is in Π2p.",

author = "Laura Giordano and Valentina Gliozzi and Nicola Olivetti and Pozzato, {Gian Luca}",

year = "2011",

doi = "10.1007/978-3-642-22119-4_15",

language = "English",

isbn = "9783642221187",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "180--195",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings",

note = "20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011 ; Conference date: 04-07-2011 Through 08-07-2011",

}

Giordano, L, Gliozzi, V, Olivetti, N & Pozzato, GL 2011, A tableau calculus for a nonmonotonic extension of ℰℒ ^⊥. in Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6793 LNAI, pagg. 180-195, 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011, Bern, Switzerland, 4/07/11. https://doi.org/10.1007/978-3-642-22119-4_15

A tableau calculus for a nonmonotonic extension of ℰℒ ^⊥. / Giordano, Laura; Gliozzi, Valentina; Olivetti, Nicola et al.
Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. 2011. pag. 180-195 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6793 LNAI).

Risultato della ricerca: Capitolo in libro/report/atti di convegno › Contributo a conferenza › peer review

TY - GEN

T1 - A tableau calculus for a nonmonotonic extension of ℰℒ ⊥

AU - Giordano, Laura

AU - Gliozzi, Valentina

AU - Olivetti, Nicola

AU - Pozzato, Gian Luca

PY - 2011

Y1 - 2011

N2 - We introduce a tableau calculus for a nonmonotonic extension of low complexity Description Logic ℰℒ⊥ that can be used to reason about typicality and defeasible properties. The calculus deals with Left Local knowledge bases in the logic ℰℒ⊥Tmin recently introduced in [8]. The calculus performs a two-phase computation to check whether a query is minimally entailed from the initial knowledge base. It is sound, complete and terminating. Furthermore, it is a decision procedure for Left Local ℰℒ⊥Tmin knowledge bases, whose complexity matches the known results for the logic, namely that entailment is in Π2p.

AB - We introduce a tableau calculus for a nonmonotonic extension of low complexity Description Logic ℰℒ⊥ that can be used to reason about typicality and defeasible properties. The calculus deals with Left Local knowledge bases in the logic ℰℒ⊥Tmin recently introduced in [8]. The calculus performs a two-phase computation to check whether a query is minimally entailed from the initial knowledge base. It is sound, complete and terminating. Furthermore, it is a decision procedure for Left Local ℰℒ⊥Tmin knowledge bases, whose complexity matches the known results for the logic, namely that entailment is in Π2p.

UR - http://www.scopus.com/inward/record.url?scp=79959687741&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-22119-4_15

DO - 10.1007/978-3-642-22119-4_15

M3 - Conference contribution

AN - SCOPUS:79959687741

SN - 9783642221187

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 180

EP - 195

BT - Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings

T2 - 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011

Y2 - 4 July 2011 through 8 July 2011

ER -

Giordano L, Gliozzi V, Olivetti N, Pozzato GL. A tableau calculus for a nonmonotonic extension of ℰℒ ^⊥. In Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. 2011. pag. 180-195. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-22119-4_15