Extending Unification in EL to Disunification: The Case of Dismatching and Local Disunification

Franz BaaderFranz Baader, Stefan BorgwardtStefan Borgwardt, Barbara MorawskaBarbara Morawska

Franz Baader, Stefan Borgwardt, Barbara Morawska
Extending Unification in EL to Disunification: The Case of Dismatching and Local Disunification
Logical Methods of Computer Science, 12(4:1):1–28, 2016

Details
Bibtex

KurzfassungAbstract
Unification in Description Logics has been introduced as a means to detect redundancies in ontologies. We try to extend the known decidability results for unification in the Description Logic EL to disunification since negative constraints can be used to avoid unwanted unifiers. While decidability of the solvability of general EL-disunification problems remains an open problem, we obtain NP-completeness results for two interesting special cases: dismatching problems, where one side of each negative constraint must be ground, and local solvability of disunification problems, where we consider only solutions that are constructed from terms occurring in the input problem. More precisely, we first show that dismatching can be reduced to local disunification, and then provide two complementary NP-algorithms for finding local solutions of disunification problems.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{BBM2016,
  author  = {Franz Baader and Stefan Borgwardt and Barbara Morawska},
  title   = {Extending Unification in {EL} to Disunification: The Case of
             Dismatching and Local Disunification},
  journal = {Logical Methods of Computer Science},
  volume  = {12},
  number  = {4:1},
  year    = {2016},
  pages   = {1{\textendash}28},
  doi     = {10.2168/LMCS-12(4:1)2016}
}