From Tableaux to Automata for Description Logics

Franz BaaderFranz Baader, J. HladikJ. Hladik, Carsten LutzCarsten Lutz, Frank WolterFrank Wolter

Datei:BaaHlaLutWol-LPAR03.ps.gz

Download

Franz Baader, J. Hladik, Carsten Lutz, Frank Wolter
From Tableaux to Automata for Description Logics
In Moshe Vardi and Andrei Voronkov, eds., Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2003), volume 2850 of Lecture Notes in Computer Science, 1-32, 2003. Springer

Details
Bibtex

KurzfassungAbstract
This paper investigates the relationship between automata- and tableau-based inference procedures for Description Logics. To be more precise, we develop an abstract notion of what a tableau-based algorithm is, and then show, on this abstract level, how tableau-based algorithms can be converted into automata-based algorithms. In particular, this allows us to characterize a large class of tableau-based algorithms that imply an ExpTime upper-bound for reasoning in the description logics for which such an algorithm exists.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BaaHlaLutWol-LPAR03,
  author = {F. {Baader} and J. {Hladik} and C. {Lutz} and F. {Wolter}},
  booktitle = {Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning ({LPAR 2003})},
  editor = {Moshe {Vardi} and Andrei {Voronkov}},
  pages = {1--32},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {From Tableaux to Automata for Description Logics},
  volume = {2850},
  year = {2003},
}