Computing Minimal EL-unifiers is Hard

Franz BaaderFranz Baader, Stefan BorgwardtStefan Borgwardt, Barbara MorawskaBarbara Morawska

Download

Franz Baader, Stefan Borgwardt, Barbara Morawska
Computing Minimal EL-unifiers is Hard
In Silvio Ghilardi and Lawrence Moss, eds., Proceedings of the 9-th International Conference on Advances in Modal Logic (AiML'12), 2012

Details
Bibtex

KurzfassungAbstract
Unification has been investigated both in modal logics and in description logics, albeit with different motivations. In description logics, unification can be used to detect redundancies in ontologies. In this context, it is not sufficient to decide unifiability, one must also compute appropriate unifiers and present them to the user. For the description logic EL, which is used to define several large biomedical ontologies, deciding unifiability is an NP-complete problem. It is known that every solvable EL-unification problem has a minimal unifier, and that every minimal unifier is a local unifier. Existing unification algorithms for EL compute all minimal unifiers, but additionally (all or some) non-minimal local unifiers. Computing only the minimal unifiers would be better since there are considerably less minimal unifiers than local ones, and their size is usually also quite small. In this paper we investigate the question whether the known algorithms for EL-unification can be modified such that they compute exactly the minimal unifiers without changing the complexity and the basic nature of the algorithms. Basically, the answer we give to this question is negative.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@inproceedings{ BaBM-AiML12,
  author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}},
  booktitle = {Proceedings of the 9-th International Conference on Advances in Modal Logic ({AiML'12})},
  editor = {Silvio {Ghilardi} and Lawrence {Moss}},
  title = {Computing Minimal {$\mathcal{EL}$}-unifiers is Hard},
  year = {2012},
}