We introduce a tableau calculus for a nonmonotonic extension of low complexity Description Logic EL\bot that can be used to reason about typicality and defeasible properties. The calculus deals with Left Local knowledge bases in the logic EL\botTmin recently introduced. 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 EL\botTmin knowledge bases, whose complexity matches the known results for the logic, namely that entailment is in \Pi^p_2 .
A tableau calculus for a nonmonotonic extension of EL^\bot
GLIOZZI, Valentina;POZZATO, GIAN LUCA
2011-01-01
Abstract
We introduce a tableau calculus for a nonmonotonic extension of low complexity Description Logic EL\bot that can be used to reason about typicality and defeasible properties. The calculus deals with Left Local knowledge bases in the logic EL\botTmin recently introduced. 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 EL\botTmin knowledge bases, whose complexity matches the known results for the logic, namely that entailment is in \Pi^p_2 .
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
TABLEAUX 2011 - DLs.pdf
Accesso riservato
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
346.85 kB
Formato
Adobe PDF
|
346.85 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
