From Tableaux to Automata for Description Logics

Franz BaaderFranz Baader, Jan HladikJan Hladik, Carsten LutzCarsten Lutz, Frank WolterFrank Wolter

Datei:BaaHlaLutWol-FI-03.ps.gz

Download

Franz Baader, Jan Hladik, Carsten Lutz, Frank Wolter
From Tableaux to Automata for Description Logics
Fundamenta Informaticae, 57:1-33, 2003

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

@article{ BaaHlaLutWol-FI-03,
  author = {Franz {Baader} and Jan {Hladik} and Carsten {Lutz} and Frank {Wolter}},
  journal = {Fundamenta Informaticae},
  pages = {1--33},
  title = {From Tableaux to Automata for Description Logics},
  volume = {57},
  year = {2003},
}