Axiom pinpointing has been introduced in description logics (DLs) to help the user to understand the reasons why consequences hold and to remove unwanted consequences by computing minimal (maximal) subsets of the knowledge base that have (do not have) the consequence in question. The pinpointing algorithms described in the DL literature are obtained as extensions of the standard tableau-based reasoning algorithms for computing consequences from DL knowledge bases. Although these extensions are based on similar ideas, they are all introduced for a particular tableau-based algorithm for a particular DL. The purpose of this paper is to develop a general approach for extending a tableau-based algorithm to a pinpointing algorithm. This approach is based on a general definition of “tableaux algorithms,” which captures many of the known tableau-based algorithms employed in DLs, but also other kinds of reasoning procedures.

Baader, F., Penaloza, R. (2007). Axiom pinpointing in general tableaux. In Automated Reasoning with Analytic Tableaux and Related Methods: 16th International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007. Proceedings (pp.11-27). Springer-Verlag [10.1007/978-3-540-73099-6_4].

Axiom pinpointing in general tableaux

Penaloza, R
2007

Abstract

Axiom pinpointing has been introduced in description logics (DLs) to help the user to understand the reasons why consequences hold and to remove unwanted consequences by computing minimal (maximal) subsets of the knowledge base that have (do not have) the consequence in question. The pinpointing algorithms described in the DL literature are obtained as extensions of the standard tableau-based reasoning algorithms for computing consequences from DL knowledge bases. Although these extensions are based on similar ideas, they are all introduced for a particular tableau-based algorithm for a particular DL. The purpose of this paper is to develop a general approach for extending a tableau-based algorithm to a pinpointing algorithm. This approach is based on a general definition of “tableaux algorithms,” which captures many of the known tableau-based algorithms employed in DLs, but also other kinds of reasoning procedures.
paper
axiom pinpointing, description logics, tableaux
English
International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2007)
2007
Olivetti, N
Automated Reasoning with Analytic Tableaux and Related Methods: 16th International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007. Proceedings
978-3-540-73098-9
2007
4548
11
27
reserved
Baader, F., Penaloza, R. (2007). Axiom pinpointing in general tableaux. In Automated Reasoning with Analytic Tableaux and Related Methods: 16th International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007. Proceedings (pp.11-27). Springer-Verlag [10.1007/978-3-540-73099-6_4].
File in questo prodotto:
File Dimensione Formato  
BaaderPenaloza-Tableaux-07.pdf

Solo gestori archivio

Tipologia di allegato: Author’s Accepted Manuscript, AAM (Post-print)
Dimensione 233.15 kB
Formato Adobe PDF
233.15 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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/238360
Citazioni
  • Scopus 34
  • ???jsp.display-item.citation.isi??? 18
Social impact