SAT Encoding of Unification in EL

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

„October“ befindet sich nicht in der Liste (Januar, Februar, März, April, Mai, Juni, Juli, August, September, Oktober, ...) zulässiger Werte für das Attribut „Month“.

Toggle side column

SAT Encoding of Unification in EL

Franz BaaderFranz Baader,  Barbara MorawskaBarbara Morawska
Franz Baader, Barbara Morawska
SAT Encoding of Unification in EL
In Christian G. Fermüller and Andrei Voronkov, eds., Proceedings of the 17th International Conference on Logic for Programming, Artifical Intelligence, and Reasoning (LPAR-17), volume 6397 of Lecture Notes in Computer Science (subline Advanced Research in Computing and Software Science), 97-111,  2010. Springer
  • KurzfassungAbstract
    Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. In a recent paper, we have shown that unification in EL is NP-complete, and thus of a complexity that is considerably lower than in other Description Logics of comparably restricted expressive power. In this paper, we introduce a new NP-algorithm for solving unification problems in EL, which is based on a reduction to satisfiability in propositional logic (SAT). The advantage of this new algorithm is, on the one hand, that it allows us to employ highly optimized state-of-the-art SAT solvers when implementing an EL-unification algorithm. On the other hand, this reduction provides us with a proof of the fact that EL-unification is in NP that is much simpler than the one given in our previous paper on EL-unification.
  • Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
The final publication is available at Springer.
@inproceedings{ BaMo-LPAR-10,
  address = {Yogyakarta, Indonesia},
  author = {Franz {Baader} and Barbara {Morawska}},
  booktitle = {Proceedings of the 17th International Conference on Logic for Programming, Artifical Intelligence, and Reasoning ({LPAR-17})},
  editor = {Christian G. {Ferm{\"u}ller} and Andrei {Voronkov}},
  month = {October},
  pages = {97--111},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science (subline Advanced Research in Computing and Software Science)},
  title = {SAT Encoding of Unification in EL},
  volume = {6397},
  year = {2010},
}