Axiom Pinpointing in General Tableaux

Franz BaaderFranz Baader, Rafael PeñalozaRafael Peñaloza

Download

Franz Baader, Rafael Peñaloza
Axiom Pinpointing in General Tableaux
In N. Olivetti, eds., Proceedings of the 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods TABLEAUX 2007, volume 4548 of Lecture Notes in Computer Science, 11-27, 2007. Springer

Details
Bibtex

KurzfassungAbstract
Axiom pinpointing has been introduced in description logics 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.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BaaderPenaloza-Tableaux-07,
  address = {Aix-en-Provence, France},
  author = {Franz {Baader} and Rafael {Pe{\~n}aloza}},
  booktitle = {Proceedings of the 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods {TABLEAUX 2007}},
  editor = {N. {Olivetti}},
  pages = {11--27},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Axiom Pinpointing in General Tableaux},
  volume = {4548},
  year = {2007},
}