Axiom pinpointing has been introduced in description logics (DL) to help the user understand the reasons why consequences hold by computing minimal subsets of the knowledge base that have the consequence in question (MinA). Most of the pinpointing algorithms described in the DL literature are obtained as extensions of tableau-based reasoning algorithms for computing consequences from DL knowledge bases. In this paper, we show that automata-based algorithms for reasoning in DLs and other logics can also be extended to pinpointing algorithms. The idea is that the tree automaton constructed by the automata-based approach can be transformed into a weighted tree automaton whose so-called behaviour yields a pinpointing formula, i.e., a monotone Boolean formula whose minimal valuations correspond to the MinAs. We also develop an approach for computing the behaviour of a given weighted tree automaton. We use the DL SI as well as Linear Temporal Logic (LTL) to illustrate our new pinpointing approach.
Baader, F., Penaloza, R. (2010). Automata-based axiom pinpointing. JOURNAL OF AUTOMATED REASONING, 45(2), 91-129 [10.1007/s10817-010-9181-2].
Automata-based axiom pinpointing
Penaloza, R
2010
Abstract
Axiom pinpointing has been introduced in description logics (DL) to help the user understand the reasons why consequences hold by computing minimal subsets of the knowledge base that have the consequence in question (MinA). Most of the pinpointing algorithms described in the DL literature are obtained as extensions of tableau-based reasoning algorithms for computing consequences from DL knowledge bases. In this paper, we show that automata-based algorithms for reasoning in DLs and other logics can also be extended to pinpointing algorithms. The idea is that the tree automaton constructed by the automata-based approach can be transformed into a weighted tree automaton whose so-called behaviour yields a pinpointing formula, i.e., a monotone Boolean formula whose minimal valuations correspond to the MinAs. We also develop an approach for computing the behaviour of a given weighted tree automaton. We use the DL SI as well as Linear Temporal Logic (LTL) to illustrate our new pinpointing approach.File | Dimensione | Formato | |
---|---|---|---|
Baader-2010-J Automated Reason-AAM.pdf
accesso aperto
Descrizione: Article
Tipologia di allegato:
Author’s Accepted Manuscript, AAM (Post-print)
Licenza:
Altro
Dimensione
410.96 kB
Formato
Adobe PDF
|
410.96 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.