Abstract
Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. In a recent paper, we have shown that unification in \(\mathcal{EL}\) is NP-complete, and thus of a complexity that is considerably lower than in other Description Logics of comparably restricted expressive power. In this paper, we introduce a new NP-algorithm for solving unification problems in \(\mathcal{EL}\), which is based on a reduction to satisfiability in propositional logic (SAT). The advantage of this new algorithm is, on the one hand, that it allows us to employ highly optimized state-of-the-art SAT solvers when implementing an \(\mathcal{EL}\)-unification algorithm. On the other hand, this reduction provides us with a proof of the fact that \(\mathcal{EL}\)-unification is in NP that is much simpler than the one given in our previous paper on \(\mathcal{EL}\)-unification.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baader, F.: Terminological cycles in a description logic with existential restrictions. In: Proc. IJCAI 2003. Morgan Kaufmann, Los Altos (2003)
Baader, F., Brandt, S., Lutz, C.: Pushing the \(\mathcal{EL}\) envelope. In: Proc. IJCAI 2005. Morgan Kaufmann, Los Altos (2005)
Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)
Baader, F., Morawska, B.: Unification in the description logic \(\mathcal{EL}\). In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 350–364. Springer, Heidelberg (2009)
Baader, F., Morawska, B.: Unification in the description logic \(\mathcal{EL}\). In: Logical Methods in Computer Science (to appear, 2010)
Baader, F., Narendran, P.: Unification of concepts terms in description logics. J. of Symbolic Computation 31(3), 277–305 (2001)
Baader, F., Schulz, K.: Unification in the union of disjoint equational theories: Combining decision procedures. J. of Symbolic Computation 21(2), 211–243 (1996)
Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning, vol. I. Elsevier Science Publishers, Amsterdam (2001)
Kapur, D., Narendran, P.: Complexity of unification problems with associative-commutative operators. J. Automated Reasoning 9, 261–288 (1992)
Küsters, R. (ed.): Non-Standard Inferences in Description Logics. LNCS (LNAI), vol. 2100, p. 33. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baader, F., Morawska, B. (2010). SAT Encoding of Unification in \(\mathcal{EL}\) . In: Fermüller, C.G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science, vol 6397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16242-8_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-16242-8_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16241-1
Online ISBN: 978-3-642-16242-8
eBook Packages: Computer ScienceComputer Science (R0)