Document Open Access Logo

Dismatching and Local Disunification in EL

Authors Franz Baader, Stefan Borgwardt, Barbara Morawska

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.40.pdf
  • Filesize: 0.57 MB
  • 17 pages

Document Identifiers

Author Details

Franz Baader
Stefan Borgwardt
Barbara Morawska

Cite AsGet BibTex

Franz Baader, Stefan Borgwardt, and Barbara Morawska. Dismatching and Local Disunification in EL. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 40-56, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.RTA.2015.40

Abstract

Unification in Description Logics has been introduced as a means to detect redundancies in ontologies. We try to extend the known decidability results for unification in the Description Logic EL to disunification since negative constraints on unifiers can be used to avoid unwanted unifiers. While decidability of the solvability of general EL-disunification problems remains an open problem, we obtain NP-completeness results for two interesting special cases: dismatching problems, where one side of each negative constraint must be ground, and local solvability of disunification problems, where we restrict the attention to solutions that are built from so-called atoms occurring in the input problem. More precisely, we first show that dismatching can be reduced to local disunification, and then provide two complementary NP-algorithms for finding local solutions of (general) disunification problems.
Keywords
  • Unification
  • Description Logics
  • SAT

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Franz Baader, Stefan Borgwardt, Julian Alfredo Mendez, and Barbara Morawska. UEL: Unification solver for EL. In Proc. DL'12, volume 846 of CEUR-WS, pages 26-36, 2012. Google Scholar
  2. Franz Baader, Stefan Borgwardt, and Barbara Morawska. Computing minimal EL-unifiers is hard. In Proc. AiML'12, 2012. Google Scholar
  3. Franz Baader, Stefan Borgwardt, and Barbara Morawska. A goal-oriented algorithm for unification in EL w.r.t. cycle-restricted TBoxes. In Proc. DL'12, volume 846 of CEUR-WS, pages 37-47, 2012. Google Scholar
  4. Franz Baader, Stefan Borgwardt, and Barbara Morawska. Dismatching and local disunfication in EL. LTCS-Report 15-03, Chair for Automata Theory, TU Dresden, Germany, 2015. See URL: http://lat.inf.tu-dresden.de/research/reports.html.
  5. Franz Baader, Sebastian Brandt, and Carsten Lutz. Pushing the EL envelope further. In Proc. OWLED'08, 2008. Google Scholar
  6. Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003. Google Scholar
  7. Franz Baader, Ralf Küsters, Alex Borgida, and Deborah L. McGuinness. Matching in description logics. J. Logic Comput., 9(3):411-447, 1999. Google Scholar
  8. Franz Baader, Ralf Küsters, and Ralf Molitor. Computing least common subsumers in description logics with existential restrictions. In Proc. IJCAI'99, pages 96-101. Morgan Kaufmann, 1999. Google Scholar
  9. Franz Baader and Barbara Morawska. SAT encoding of unification in EL. In Proc. LPAR'10, volume 6397 of LNCS, pages 97-111. Springer, 2010. Google Scholar
  10. Franz Baader and Barbara Morawska. Unification in the description logic EL. Log. Meth. Comput. Sci., 6(3), 2010. Google Scholar
  11. Franz Baader and Barbara Morawska. Matching with respect to general concept inclusions in the description logic EL. In Proc. KI'14, volume 8736 of LNCS, pages 135-146. Springer, 2014. Google Scholar
  12. Franz Baader and Paliath Narendran. Unification of concept terms in description logics. J. Symb. Comput., 31(3):277-305, 2001. Google Scholar
  13. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1999. Google Scholar
  14. Franz Baader and Alexander Okhotin. Solving language equations and disequations with applications to disunification in description logics and monadic set constraints. In Proc. LPAR'12, volume 7180 of LNCS, pages 107-121. Springer, 2012. Google Scholar
  15. Sergey Babenyshev, Vladimir V. Rybakov, Renate Schmidt, and Dmitry Tishkovsky. A tableau method for checking rule admissibility in S4. In Proc. M4M-6, 2009. Google Scholar
  16. Sebastian Brandt. Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and - what else? In Proc. ECAI'04, pages 298-302, 2004. Google Scholar
  17. Wray L. Buntine and Hans-Jürgen Bürckert. On solving equations and disequations. J. of the ACM, 41(4):591-629, 1994. Google Scholar
  18. Hubert Comon. Disunification: A survey. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 322-359. MIT Press, 1991. Google Scholar
  19. Silvio Ghilardi. Unification through projectivity. J. Logic and Computation, 7(6):733-752, 1997. Google Scholar
  20. Silvio Ghilardi. Unification in intuitionistic logic. J. Logic and Computation, 64(2):859-880, 1999. Google Scholar
  21. Ian Horrocks, Peter F. Patel-Schneider, and Frank van Harmelen. From SHIQ and RDF to OWL: The making of a web ontology language. J. Web Sem., 1(1):7-26, 2003. Google Scholar
  22. Rosalie Iemhoff and George Metcalfe. Proof theory for admissible rules. Ann. Pure Appl. Logic, 159(1-2):171-186, 2009. Google Scholar
  23. Ralf Küsters. Chapter 6: Matching. In Non-Standard Inferences in Description Logics, volume 2100 of LNCS, pages 153-227. Springer, 2001. Google Scholar
  24. Vladimir V. Rybakov. Admissibility of logical inference rules, volume 136 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 1997. Google Scholar
  25. Vladimir V. Rybakov. Multi-modal and temporal logics with universal formula - reduction of admissibility to validity and unification. J. Logic and Computation, 18(4):509-519, 2008. Google Scholar
  26. Klaus Schild. A correspondence theory for terminological logics: Preliminary report. In Proc. IJCAI'91, pages 466-471, 1991. Google Scholar
  27. Frank Wolter and Michael Zakharyaschev. Undecidability of the unification and admissibility problems for modal and description logics. ACM Trans. Comput. Log., 9(4), 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact