# Computing Minimal EL-unifiers is Hard

From International Center for Computational Logic

# Computing Minimal EL-unifiers is Hard

##### Franz BaaderFranz Baader, Stefan BorgwardtStefan Borgwardt, Barbara MorawskaBarbara Morawska

Franz Baader, Stefan Borgwardt, Barbara Morawska

In Silvio Ghilardi and Lawrence Moss, eds.,

**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**Kurzfassung****Abstract**

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:**Automatentheorie

```
@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},
}
```