Blocking and Pinpointing in Forest Tableaux

Franz BaaderFranz Baader, Rafael PeñalozaRafael Peñaloza

Download

Franz Baader, Rafael Peñaloza
Blocking and Pinpointing in Forest Tableaux
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, volume LTCS-08-02, 2008. LTCS-Report

Details
Bibtex

KurzfassungAbstract
Axiom pinpointing has been introduced in Description Logics (DLs) to help the used understand the reasons why consequences hold by computing minimal subsets of the knowledge base that have the consequence in consideration. Several pinpointing algorithms have been described as extensions of the standard tableau-based reasoning algorithms for deciding 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, using specific traits of them. In the past, we have developed a general approach for extending tableau-based algorithms into pinpointing algorithms. In this paper we explore some issues of termination of general tableaux and their pinpointing extensions. We also define a subclass of tableaux that allows the use of so-called blocking conditions, which stop the execution of the algorithm once a pattern is found, and adapt the pinpointing extensions accordingly, guaranteeing its correctness and termination.
Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ BaPe-LTCS-07-01,
  address = {Germany},
  author = {Franz {Baader} and Rafael {Pe{\~n}aloza}},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {LTCS-08-02},
  title = {Blocking and Pinpointing in Forest Tableaux},
  type = {LTCS-Report},
  year = {2008},
}