Skip to main content

2017 | OriginalPaper | Buchkapitel

Lean Kernels in Description Logics

verfasst von : Rafael Peñaloza, Carlos Mencía, Alexey Ignatiev, Joao Marques-Silva

Erschienen in: The Semantic Web

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Lean kernels (LKs) are an effective optimization for deriving the causes of unsatisfiability of a propositional formula. Interestingly, no analogous notion exists for explaining consequences of description logic (DL) ontologies. We introduce LKs for DLs using a general notion of consequence-based methods, and provide an algorithm for computing them which incurs in only a linear time overhead. As an example, we instantiate our framework to the DL \({\mathcal {ALC}}\). We prove formally and empirically that LKs provide a tighter approximation of the set of relevant axioms for a consequence than syntactic locality-based modules.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
Finding the union of MUSes is at least as hard as testing MUS membership, which is \(\Sigma _2^{p}\)-complete for arbitrary CNF formulas [23, Theorem 4].
 
Literatur
1.
Zurück zum Zitat Arif, M.F., Mencía, C., Ignatiev, A., Manthey, N., Peñaloza, R., Marques-Silva, J.: BEACON: An efficient SAT-based tool for debugging EL+ ontologies. In: SAT, pp. 521–530 (2016) Arif, M.F., Mencía, C., Ignatiev, A., Manthey, N., Peñaloza, R., Marques-Silva, J.: BEACON: An efficient SAT-based tool for debugging EL+ ontologies. In: SAT, pp. 521–530 (2016)
2.
Zurück zum Zitat Romero, A.A.: Ontology module extraction and applications to ontology classification. Ph.D. thesis, University of Oxford, UK (2015) Romero, A.A.: Ontology module extraction and applications to ontology classification. Ph.D. thesis, University of Oxford, UK (2015)
3.
Zurück zum Zitat Romero, A.A., Kaminski, M., Grau, B.C., Horrocks, I.: Ontology module extraction via datalog reasoning. In: AAAI, pp. 1410–1416 (2015) Romero, A.A., Kaminski, M., Grau, B.C., Horrocks, I.: Ontology module extraction via datalog reasoning. In: AAAI, pp. 1410–1416 (2015)
4.
Zurück zum Zitat Romero, A.A., Kaminski, M., Cuenca Grau, B., Horrocks, I.: Module extraction in expressive ontology languages via datalog reasoning. JAIR 55, 499–564 (2016)MathSciNetMATH Romero, A.A., Kaminski, M., Cuenca Grau, B., Horrocks, I.: Module extraction in expressive ontology languages via datalog reasoning. JAIR 55, 499–564 (2016)MathSciNetMATH
5.
Zurück zum Zitat Baader, F., Brandt, S., Lutz, C.: Pushing the \(\cal{E\!L}\) envelope. In: IJCAI, pp. 364–369 (2005) Baader, F., Brandt, S., Lutz, C.: Pushing the \(\cal{E\!L}\) envelope. In: IJCAI, pp. 364–369 (2005)
6.
Zurück zum Zitat 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)MATH 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)MATH
7.
Zurück zum Zitat Baader, F., Knechtel, M., Peñaloza, R.: Context-dependent views to axioms and consequences of semantic web ontologies. J. Web Semant. 12–13, 22–40 (2012)CrossRef Baader, F., Knechtel, M., Peñaloza, R.: Context-dependent views to axioms and consequences of semantic web ontologies. J. Web Semant. 12–13, 22–40 (2012)CrossRef
8.
Zurück zum Zitat Baader, F., Suntisrivaraporn, B.: Debugging SNOMED CT using axiom pinpointing in the description logic \(\cal{EL}^{+}\). In: KR-MED (2008) Baader, F., Suntisrivaraporn, B.: Debugging SNOMED CT using axiom pinpointing in the description logic \(\cal{EL}^{+}\). In: KR-MED (2008)
9.
Zurück zum Zitat Bate, A., Motik, B., Grau, B.C., Simancik, F., Horrocks, I.: Extending consequence-based reasoning to SRIQ. In: KR, pp. 187–196 (2016) Bate, A., Motik, B., Grau, B.C., Simancik, F., Horrocks, I.: Extending consequence-based reasoning to SRIQ. In: KR, pp. 187–196 (2016)
10.
Zurück zum Zitat Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97–116 (2012)MathSciNetMATH Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97–116 (2012)MathSciNetMATH
11.
12.
Zurück zum Zitat Grau, B.C., Horrocks, I., Kazakov, Y., Sattler, U.: Just the right amount: Extracting modules from ontologies. In: WWW, pp. 717–726 (2007) Grau, B.C., Horrocks, I., Kazakov, Y., Sattler, U.: Just the right amount: Extracting modules from ontologies. In: WWW, pp. 717–726 (2007)
13.
Zurück zum Zitat Cuenca Grau, B., Horrocks, I., Kazakov, Y., Sattler, U.: Modular reuse of ontologies: Theory and practice. J. Artif. Intell. Res. (JAIR) 31, 273–318 (2008)MathSciNetMATH Cuenca Grau, B., Horrocks, I., Kazakov, Y., Sattler, U.: Modular reuse of ontologies: Theory and practice. J. Artif. Intell. Res. (JAIR) 31, 273–318 (2008)MathSciNetMATH
14.
Zurück zum Zitat Cuenca Grau, B., Horrocks, I., Kazakov, Y., Sattler, U.: Extracting modules from ontologies: A logic-based approach. In: Stuckenschmidt, H., Parent, C., Spaccapietra, S. (eds.) Modular Ontologies. LNCS, vol. 5445, pp. 159–186. Springer, Heidelberg (2009). doi:10.1007/978-3-642-01907-4_8CrossRefMATH Cuenca Grau, B., Horrocks, I., Kazakov, Y., Sattler, U.: Extracting modules from ontologies: A logic-based approach. In: Stuckenschmidt, H., Parent, C., Spaccapietra, S. (eds.) Modular Ontologies. LNCS, vol. 5445, pp. 159–186. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-01907-4_​8CrossRefMATH
15.
Zurück zum Zitat Vescovo, C., Klinov, P., Parsia, B., Sattler, U., Schneider, T., Tsarkov, D.: Empirical study of logic-based modules: Cheap is cheerful. In: Alani, H., Kagal, L., Fokoue, A., Groth, P., Biemann, C., Parreira, J.X., Aroyo, L., Noy, N., Welty, C., Janowicz, K. (eds.) ISWC 2013. LNCS, vol. 8218, pp. 84–100. Springer, Heidelberg (2013). doi:10.1007/978-3-642-41335-3_6CrossRef Vescovo, C., Klinov, P., Parsia, B., Sattler, U., Schneider, T., Tsarkov, D.: Empirical study of logic-based modules: Cheap is cheerful. In: Alani, H., Kagal, L., Fokoue, A., Groth, P., Biemann, C., Parreira, J.X., Aroyo, L., Noy, N., Welty, C., Janowicz, K. (eds.) ISWC 2013. LNCS, vol. 8218, pp. 84–100. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-41335-3_​6CrossRef
16.
Zurück zum Zitat Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of OWL DL entailments. In: Aberer, K., Choi, K.-S., Noy, N., Allemang, D., Lee, K.-I., Nixon, L., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., Cudré-Mauroux, P. (eds.) ASWC/ISWC -2007. LNCS, vol. 4825, pp. 267–280. Springer, Heidelberg (2007). doi:10.1007/978-3-540-76298-0_20CrossRef Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of OWL DL entailments. In: Aberer, K., Choi, K.-S., Noy, N., Allemang, D., Lee, K.-I., Nixon, L., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., Cudré-Mauroux, P. (eds.) ASWC/ISWC -2007. LNCS, vol. 4825, pp. 267–280. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-76298-0_​20CrossRef
17.
Zurück zum Zitat Kaminski, M., Nenov, Y., Grau, B.C.: Datalog rewritability of disjunctive datalog programs and its applications to ontology reasoning. In: AAAI, pp. 1077–1083 (2014) Kaminski, M., Nenov, Y., Grau, B.C.: Datalog rewritability of disjunctive datalog programs and its applications to ontology reasoning. In: AAAI, pp. 1077–1083 (2014)
18.
Zurück zum Zitat Kazakov, Y.: Consequence-driven reasoning for Horn SHIQ ontologies. In: Boutilier, C. (ed.) IJCAI 2009, pp. 2040–2045 (2009) Kazakov, Y.: Consequence-driven reasoning for Horn SHIQ ontologies. In: Boutilier, C. (ed.) IJCAI 2009, pp. 2040–2045 (2009)
19.
Zurück zum Zitat Kazakov, Y., Krötzsch, M., Simancik, F.: The incredible ELK - from polynomial procedures to efficient reasoning with \(\cal{E\!L}\) ontologies. JAR 53(1), 1–61 (2014)MathSciNetCrossRef Kazakov, Y., Krötzsch, M., Simancik, F.: The incredible ELK - from polynomial procedures to efficient reasoning with \(\cal{E\!L}\) ontologies. JAR 53(1), 1–61 (2014)MathSciNetCrossRef
20.
Zurück zum Zitat Büning, H.K., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 339–401. IOS Press (2009) Büning, H.K., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 339–401. IOS Press (2009)
21.
22.
Zurück zum Zitat Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 22–35. Springer, Heidelberg (2006). doi:10.1007/11814948_4CrossRefMATH Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 22–35. Springer, Heidelberg (2006). doi:10.​1007/​11814948_​4CrossRefMATH
23.
24.
Zurück zum Zitat Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223–250 (2016)MathSciNetCrossRef Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223–250 (2016)MathSciNetCrossRef
25.
Zurück zum Zitat Liffiton, M., Sakallah, K.: Searching for autarkies to trim unsatisfiable clause sets. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 182–195. Springer, Heidelberg (2008). doi:10.1007/978-3-540-79719-7_18CrossRef Liffiton, M., Sakallah, K.: Searching for autarkies to trim unsatisfiable clause sets. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 182–195. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-79719-7_​18CrossRef
26.
Zurück zum Zitat Ludwig, M., Peñaloza, R.: Error-tolerant reasoning in the description logic \(\cal{E\!L}\). In: JELIA, pp. 107–121 (2014) Ludwig, M., Peñaloza, R.: Error-tolerant reasoning in the description logic \(\cal{E\!L}\). In: JELIA, pp. 107–121 (2014)
27.
Zurück zum Zitat Marques-Silva, J., Ignatiev, A., Mencía, C., Peñaloza, R.: Efficient reasoning for inconsistent horn formulae. In: Michael, L., Kakas, A. (eds.) JELIA 2016. LNCS (LNAI), vol. 10021, pp. 336–352. Springer, Cham (2016). doi:10.1007/978-3-319-48758-8_22CrossRef Marques-Silva, J., Ignatiev, A., Mencía, C., Peñaloza, R.: Efficient reasoning for inconsistent horn formulae. In: Michael, L., Kakas, A. (eds.) JELIA 2016. LNCS (LNAI), vol. 10021, pp. 336–352. Springer, Cham (2016). doi:10.​1007/​978-3-319-48758-8_​22CrossRef
28.
Zurück zum Zitat Marques-Silva, J., Ignatiev, A., Morgado, A., Manquinho, V.M., Lynce, I.: Efficient autarkies. In: ECAI, pp. 603–608 (2014) Marques-Silva, J., Ignatiev, A., Morgado, A., Manquinho, V.M., Lynce, I.: Efficient autarkies. In: ECAI, pp. 603–608 (2014)
29.
Zurück zum Zitat Minoux, M.: LTUR: A simplified linear-time unit resolution algorithm for horn formulae and computer implementation. Inf. Process. Lett. 29(1), 1–12 (1988)MathSciNetCrossRef Minoux, M.: LTUR: A simplified linear-time unit resolution algorithm for horn formulae and computer implementation. Inf. Process. Lett. 29(1), 1–12 (1988)MathSciNetCrossRef
30.
Zurück zum Zitat Peñaloza, R., Sertkaya, B.: On the complexity of axiom pinpointing in the \(\cal{E\!L}\) family of description logics. In: KR (2010) Peñaloza, R., Sertkaya, B.: On the complexity of axiom pinpointing in the \(\cal{E\!L}\) family of description logics. In: KR (2010)
31.
Zurück zum Zitat Riguzzi, F., Bellodi, E., Lamma, E., Zese, R.: Probabilistic description logics under the distribution semantics. Semant. Web 6(5), 477–501 (2015)CrossRef Riguzzi, F., Bellodi, E., Lamma, E., Zese, R.: Probabilistic description logics under the distribution semantics. Semant. Web 6(5), 477–501 (2015)CrossRef
32.
Zurück zum Zitat Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with complements. Artif. Intell. 48(1), 1–26 (1991)MathSciNetCrossRef Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with complements. Artif. Intell. 48(1), 1–26 (1991)MathSciNetCrossRef
33.
Zurück zum Zitat Sebastiani, R., Vescovi, M.: Axiom pinpointing in lightweight description logics via horn-SAT encoding and conflict analysis. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 84–99. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02959-2_6CrossRef Sebastiani, R., Vescovi, M.: Axiom pinpointing in lightweight description logics via horn-SAT encoding and conflict analysis. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 84–99. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-02959-2_​6CrossRef
35.
Zurück zum Zitat Simancik, F., Kazakov, Y., Horrocks, I.: Consequence-based reasoning beyond horn ontologies. In: IJCAI 2011, pp. 1093–1098 (2011). IJCAI/AAAI Simancik, F., Kazakov, Y., Horrocks, I.: Consequence-based reasoning beyond horn ontologies. In: IJCAI 2011, pp. 1093–1098 (2011). IJCAI/AAAI
36.
Zurück zum Zitat Suntisrivaraporn, B.: Module extraction and incremental classification: A pragmatic approach for \(\cal{EL}^+\) ontologies. In: ESWC, pp. 230–244 (2008) Suntisrivaraporn, B.: Module extraction and incremental classification: A pragmatic approach for \(\cal{EL}^+\) ontologies. In: ESWC, pp. 230–244 (2008)
37.
Zurück zum Zitat Suntisrivaraporn, B.: Polynomial-Time Reasoning Support for Design and Maintenance of Large-Scale Biomedical Ontologies. Ph.D. thesis, TU Dresden (2009) Suntisrivaraporn, B.: Polynomial-Time Reasoning Support for Design and Maintenance of Large-Scale Biomedical Ontologies. Ph.D. thesis, TU Dresden (2009)
38.
Zurück zum Zitat Suntisrivaraporn, B., Qi, G., Ji, Q., Haase, P.: A modularization-based approach to finding all justifications for OWL DL entailments. In: Domingue, J., Anutariya, C. (eds.) ASWC 2008. LNCS, vol. 5367, pp. 1–15. Springer, Heidelberg (2008). doi:10.1007/978-3-540-89704-0_1CrossRef Suntisrivaraporn, B., Qi, G., Ji, Q., Haase, P.: A modularization-based approach to finding all justifications for OWL DL entailments. In: Domingue, J., Anutariya, C. (eds.) ASWC 2008. LNCS, vol. 5367, pp. 1–15. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-89704-0_​1CrossRef
Metadaten
Titel
Lean Kernels in Description Logics
verfasst von
Rafael Peñaloza
Carlos Mencía
Alexey Ignatiev
Joao Marques-Silva
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-58068-5_32

Neuer Inhalt