Unification in the Description Logic EL

Franz Baader; Barbara Morawska

doi:10.2168/LMCS-6(3:17)2010

Franz Baader ; Barbara Morawska - Unification in the Description Logic EL

lmcs:1106 - Logical Methods in Computer Science, September 4, 2010, Volume 6, Issue 3 - https://doi.org/10.2168/LMCS-6(3:17)2010

Unification in the Description Logic ELArticle

Authors: Franz Baader ; Barbara Morawska

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.

Comment: 31pages

https://doi.org/10.2168/LMCS-6(3:17)2010

Source: arXiv.org:1006.2289

Volume: Volume 6, Issue 3

Secondary volumes: Selected Papers of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009)

Published on: September 4, 2010

Imported on: October 21, 2009

Keywords: Computer Science - Artificial Intelligence, Computer Science - Logic in Computer Science, cs.LO

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

24 Documents citing this article

Franz Baader;Oliver Fernández Gil, 2024, Unification in the Description Logic $$\mathcal {ELH}_{\mathcal {R}^+}$$ Without the Top Concept Modulo Cycle-Restricted Ontologies, Lecture notes in computer science, pp. 279-297, 10.1007/978-3-031-63501-4_15, https://doi.org/10.1007/978-3-031-63501-4_15.

Vladimir V. Rybakov, 2022, Temporal Multi-Agents’ Logics Modelling Dynamic Temporal Accessibility Relations, Procedia Computer Science, 207, pp. 475-482, 10.1016/j.procs.2022.09.102, https://doi.org/10.1016/j.procs.2022.09.102.

Vladimir V. Rybakov, 2022, Temporal Logic in Multi-agent Environment, Smart innovation, systems and technologies, pp. 3-12, 10.1007/978-981-19-3359-2_1.

Franz Baader;Oliver Fernández Gil;Maryam Rostamigiv, 2021, Restricted Unification in the DL $$\mathcal {FL}_0$$, Lecture notes in computer science, pp. 81-97, 10.1007/978-3-030-86205-3_5.

Franz Baader;Francesco Kriegel;Adrian Nuradiansyah;Rafael Peñaloza, 2020, Computing Compliant Anonymisations of Quantified ABoxes w.r.t. $$\mathcal {EL} $$ Policies, BOA (University of Milano-Bicocca), pp. 3-20, 10.1007/978-3-030-62419-4_1, http://hdl.handle.net/10281/299177.

Pavlos Marantidis, 2020, Quantitative Variants of Language Equations and their Applications to Description Logics, KI - Künstliche Intelligenz, 34, 3, pp. 405-409, 10.1007/s13218-020-00664-9.

Franz Baader;Francesco Kriegel;Adrian Nuradiansyah, 2019, Privacy-Preserving Ontology Publishing for $$\mathcal {EL} $$ Instance Stores, Lecture notes in computer science, pp. 323-338, 10.1007/978-3-030-19570-0_21.

V. V. Rybakov, 2018, Multiagent Temporal Logics with Multivaluations, Siberian Mathematical Journal, 59, 4, pp. 710-720, 10.1134/s0037446618040134.

Christoph Wernhard, 2017, The Boolean Solution Problem from the Perspective of Predicate Logic, Lecture notes in computer science, pp. 333-350, 10.1007/978-3-319-66167-4_19.

Franz Baader;Oliver Fernández Gil;Pavlos Marantidis, 2017, Approximation in Description Logics: How Weighted Tree Automata Can Help to Define the Required Concept Comparison Measures in $$\mathcal {FL}_0$$, Lecture notes in computer science, pp. 3-26, 10.1007/978-3-319-53733-7_1.

Franz Baader;Nguyen Thanh Binh;Stefan Borgwardt;Barbara Morawska, 2016, Deciding Unifiability and Computing Local Unifiers in the Description Logic EL without Top Constructor, Notre Dame Journal of Formal Logic, 57, 4, 10.1215/00294527-3555507.

Franz Baader;Pavlos Marantidis;Alexander Okhotin, 2016, Approximate Unification in the Description Logic $$\mathcal {FL}_0$$, Lecture notes in computer science, pp. 49-63, 10.1007/978-3-319-48758-8_4.

Franz Baader;Barbara Morawska, 2014, Matching with Respect to General Concept Inclusions in the Description Logic $\mathcal{EL}$, Lecture notes in computer science, pp. 135-146, 10.1007/978-3-319-11206-0_14.

Emil Jeřábek, 2013, Blending margins: the modal logic K has nullary unification type, arXiv (Cornell University), 25, 5, pp. 1231-1240, 10.1093/logcom/ext055, http://arxiv.org/abs/1108.6240.

Franz Baader;Oliver Fernández Gil;Barbara Morawska, 2013, Hybrid Unification in the Description Logic $\mathcal{EL}$, Lecture notes in computer science, pp. 295-310, 10.1007/978-3-642-40885-4_21.

Sergei Odintsov;Vladimir Rybakov, 2013, Unification and admissible rules for paraconsistent minimal Johanssonsʼ logic J and positive intuitionistic logicIPC+, Annals of Pure and Applied Logic, 164, 7-8, pp. 771-784, 10.1016/j.apal.2013.01.001.

Franz Baader;Julian Mendez;Barbara Morawska, 2012, UEL: Unification Solver for the Description Logic $\mathcal{EL}$ – System Description, Lecture notes in computer science, pp. 45-51, 10.1007/978-3-642-31365-3_6.

Franz Baader;Stefan Borgwardt;Barbara Morawska, 2012, SAT Encoding of Unification in $\mathcal{ELH}_{{R}^+}$ w.r.t. Cycle-Restricted Ontologies, Lecture notes in computer science, pp. 30-44, 10.1007/978-3-642-31365-3_5.

Franz Baader;Stefan Borgwardt;Barbara Morawska, 2012, A Goal-Oriented Algorithm for Unification in $\mathcal{ELH}_{R+}$ w.r.t. Cycle-Restricted Ontologies, Lecture notes in computer science, pp. 493-504, 10.1007/978-3-642-35101-3_42.

George Metcalfe;Christoph Röthlisberger, 2012, Unifiability and Admissibility in Finite Algebras, Lecture notes in computer science, pp. 485-495, 10.1007/978-3-642-30870-3_49.

Franz Baader;Nguyen Thanh Binh;Stefan Borgwardt;Barbara Morawska, 2011, Unification in the Description Logic $\mathcal{EL}$ without the Top Concept, Lecture notes in computer science, pp. 70-84, 10.1007/978-3-642-22438-6_8.

Sergey Babenyshev;Vladimir Rybakov, 2011, Unification in linear temporal logic LTL, Annals of Pure and Applied Logic, 162, 12, pp. 991-1000, 10.1016/j.apal.2011.06.004.

Vladimir V. Rybakov, 2011, Best Unifiers in Transitive Modal Logics, Studia Logica, 99, 1-3, pp. 321-336, 10.1007/s11225-011-9354-y.

Franz Baader;Barbara Morawska, 2010, SAT Encoding of Unification in $\mathcal{EL}$, Lecture notes in computer science, pp. 97-111, 10.1007/978-3-642-16242-8_8.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3383 times.

This article's PDF has been downloaded 639 times.