Tableau Algorithms for Description Logics

PublikationenPublications

• Nach AutorBy Author
  • Franz BaaderFranz Baader
  • Ulrike SattlerUlrike Sattler
• Nach ForschungsgruppeBy Research Group
  • AutomatentheorieAutomata Theory

Toggle side column

Tableau Algorithms for Description Logics

Franz BaaderFranz Baader,  Ulrike SattlerUlrike Sattler

Datei:BaaderSattler-Tableaux-2000.ps.gz

• Download

Franz Baader, Ulrike Sattler
Tableau Algorithms for Description Logics
In R. Dyckhoff, eds., Proceedings of the International Conference on Automated Reasoning with Tableaux and Related Methods (Tableaux 2000), volume 1847 of Lecture Notes in Artificial Intelligence, 1-18, 2000. Springer

• Details
• Bibtex

• KurzfassungAbstract
  Description logics are a family of knowledge representation formalisms that are descended from semantic networks and frames via the system KLONE. During the last decade, it has been shown that the important reasoning problems (like subsumption and satisfiability) in a great variety of description logics can be decided using tableau-like algorithms. This is not very surprising since description logics have turned out to be closely related to propositional modal logics and logics of programs (such as propositional dynamic logic), for which tableau procedures have been quite successful. Nevertheless, due to different underlying intuitions and applications, most description logics differ significantly from run-of-the-mill modal and program logics. Consequently, the research on tableau algorithms in description logics led to new techniques and results, which are, however, also of interest for modal logicians. In this article, we will focus on three features that play an important role in description logics (number restrictions, terminological axioms, and role constructors), and show how they can be taken into account by tableau algorithms.
• Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BaaderSattler-Tablaux-2000,
  address = {St Andrews, Scotland, UK},
  author = {F. {Baader} and U. {Sattler}},
  booktitle = {Proceedings of the International Conference on Automated Reasoning with Tableaux and Related Methods (Tableaux 2000)},
  editor = {R. {Dyckhoff}},
  pages = {1--18},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Artificial Intelligence},
  title = {Tableau Algorithms for Description Logics},
  volume = {1847},
  year = {2000},
}