Unification in the Description Logic EL
The Description Logic EL has recently drawn considerable attention since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand, EL is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2010-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1106/pdf |
| _version_ | 1797268754167496704 |
|---|---|
| author | Franz Baader Barbara Morawska |
| author_facet | Franz Baader Barbara Morawska |
| author_sort | Franz Baader |
| collection | DOAJ |
| description | The Description Logic EL has recently drawn considerable attention since, on
the one hand, important inference problems such as the subsumption problem are
polynomial. On the other hand, EL is used to define large biomedical
ontologies. Unification in Description Logics has been proposed as a novel
inference service that can, for example, be used to detect redundancies in
ontologies. The main result of this paper is that unification in EL is
decidable. More precisely, EL-unification is NP-complete, and thus has the same
complexity as EL-matching. We also show that, w.r.t. the unification type, EL
is less well-behaved: it is of type zero, which in particular implies that
there are unification problems that have no finite complete set of unifiers. |
| first_indexed | 2024-04-25T01:37:30Z |
| format | Article |
| id | doaj.art-387ff54503d342b4b0a975414139b9c3 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:30Z |
| publishDate | 2010-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-387ff54503d342b4b0a975414139b9c32024-03-08T09:12:33ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742010-09-01Volume 6, Issue 310.2168/LMCS-6(3:17)20101106Unification in the Description Logic ELFranz Baaderhttps://orcid.org/0000-0002-4049-221XBarbara Morawskahttps://orcid.org/0000-0003-4724-7206The Description Logic EL has recently drawn considerable attention since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand, EL is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. The main result of this paper is that unification in EL is decidable. More precisely, EL-unification is NP-complete, and thus has the same complexity as EL-matching. We also show that, w.r.t. the unification type, EL is less well-behaved: it is of type zero, which in particular implies that there are unification problems that have no finite complete set of unifiers.https://lmcs.episciences.org/1106/pdfcomputer science - artificial intelligencecomputer science - logic in computer sciencecs.lo |
| spellingShingle | Franz Baader Barbara Morawska Unification in the Description Logic EL Logical Methods in Computer Science computer science - artificial intelligence computer science - logic in computer science cs.lo |
| title | Unification in the Description Logic EL |
| title_full | Unification in the Description Logic EL |
| title_fullStr | Unification in the Description Logic EL |
| title_full_unstemmed | Unification in the Description Logic EL |
| title_short | Unification in the Description Logic EL |
| title_sort | unification in the description logic el |
| topic | computer science - artificial intelligence computer science - logic in computer science cs.lo |
| url | https://lmcs.episciences.org/1106/pdf |
| work_keys_str_mv | AT franzbaader unificationinthedescriptionlogicel AT barbaramorawska unificationinthedescriptionlogicel |