Unification in a Description Logic with Transitive Closure of Roles

Franz BaaderFranz Baader, R. KüstersR. Küsters

Datei:BaaderKuesters-LPAR.ps.gz

Download

Franz Baader, R. Küsters
Unification in a Description Logic with Transitive Closure of Roles
In R. Nieuwenhuis and A. Voronkov, eds., Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001), volume 2250 of Lecture Notes in Computer Science, 217-232, 2001. Springer

Details
Bibtex

KurzfassungAbstract
Unification of concept descriptions was introduced by Baader and Narendran as a tool for detecting redundancies in knowledge bases. It was shown that unification in the small description logic FL0, which allows for conjunction, value restriction, and the top concept only, is already ExpTime-complete. The present paper shows that the complexity does not increase if one additionally allows for composition, union, and transitive closure of roles. It also shows that matching (which is polynomial in FL0) is PSpace-complete in the extended description logic. These results are proved via a reduction to linear equations over regular languages, which are then solved using automata. The obtained results are also of interest in formal language theory.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BaaderKuesters-LPAR,
  address = {Havana, Cuba},
  author = {F. {Baader} and R. {K{\"u}sters}},
  booktitle = {Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001)},
  editor = {R. {Nieuwenhuis} and A. {Voronkov}},
  pages = {217--232},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Unification in a Description Logic with Transitive Closure of Roles},
  volume = {2250},
  year = {2001},
}