Abstract
Axiom pinpointing consists in computing a set-wise minimal set of axioms that explains the reason for a subsumption relation in an ontology. Recently, an encoding of the classification of an \({\mathcal {EL}}^{+}\) ontology to a polynomial-size Horn propositional formula has been devised. This enables the development of a method for axiom pinpointing based on the analysis of unsatisfiable propositional formulas. Building on this earlier work, we propose a computation method, termed EL2MCS, that exploits an important relationship between minimal axiom sets and minimal unsatisfiable subformulas in the propositional domain. Experimental evaluation shows that EL2MCS achieves substantial performance gains over existing axiom pinpointing approaches for lightweight description logics.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Arif, M.F., Marques-Silva, J.: Towards efficient axiom pinpointing of \({\cal EL}^+\) ontologies. CoRR, abs/1503.08454 (2015). http://arxiv.org/abs/1503.08454
Ashburner, M., Ball, C.A., Blake, J.A., Botstein, D., Heather Butler, J., Cherry, M., Davis, A.P., Dolinski, K., Dwight, S.S., Eppig, J.T., et al.: Gene ontology: tool for the unification of biology. Nature Genetics 25(1), 25–29 (2000)
Baader, F., Brandt, S., Lutz, C.: Pushing the \({\cal EL}\) envelope. In: IJCAI, pp. 364–369 (2005)
Baader, F., Lutz, C., Suntisrivaraporn, B.: CEL — a polynomial-time reasoner for life science ontologies. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 287–291. Springer, Heidelberg (2006)
Baader, F., Peñaloza, R., Suntisrivaraporn, B.: Pinpointing in the description logic \({\cal EL}\). In: DL (2007)
Baader, F., Peñaloza, R., Suntisrivaraporn, B.: Pinpointing in the description logic \({\cal EL}^+\). In: Hertzberg, J., Beetz, M., Englert, R. (eds.) KI 2007. LNCS (LNAI), vol. 4667, pp. 52–67. Springer, Heidelberg (2007)
Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol. 3350, pp. 174–186. Springer, Heidelberg (2005)
Belov, A., Heule, M.J.H., Marques-Silva, J.: MUS extraction using clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 48–57. Springer, Heidelberg (2014)
Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97–116 (2012)
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, vol. 185 (2009)
Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15(1), 25–46 (2003)
Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD, pp. 173–180 (2007)
Hébert, C., Bretto, A., Crémilleux, B.: A data mining formalization to improve hypergraph minimal transversal computation. Fundammenta Informaticae 80(4), 415–433 (2007)
Junker, U.: QuickXplain: preferred explanations and relaxations for over-constrained problems. In: AAAI, pp. 167–172 (2004)
Kalyanpur, A., Parsia, B., Sirin, E., Cuenca-Grau, B.: Repairing unsatisfiable concepts in OWL ontologies. In: Sure, Y., Domingue, J. (eds.) ESWC 2006. LNCS, vol. 4011, pp. 170–184. Springer, Heidelberg (2006)
Lagniez, J.-M., Biere, A.: Factoring out assumptions to speed up MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 276–292. Springer, Heidelberg (2013)
Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 424–437. Springer, Heidelberg (2006)
Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1–33 (2008)
Ludwig, M.: Just: a tool for computing justifications w.r.t. EL ontologies. In: ORE 2014, vol. 1207, pp. 1–7 (2014)
Ludwig, M., Peñaloza, R.: Error-tolerant reasoning in the description logic \({\cal EL}\). In: Fermé, E., Leite, J. (eds.) JELIA 2014. LNCS, vol. 8761, pp. 107–121. Springer, Heidelberg (2014)
Malitsky, Y., O’Sullivan, B., Previti, A., Marques-Silva, J.: Timeout-sensitive portfolio approach to enumerating minimal correction subsets for satisfiability problems. In: ECAI, pp. 1065–1066 (2014)
Manthey, N., Peñaloza, R.: Exploiting SAT technology for axiom pinpointing. Technical Report LTCS 15–05, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, April 2015. https://ddll.inf.tu-dresden.de/web/Techreport3010
Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI (2013)
Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in boolean formulae. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 592–607. Springer, Heidelberg (2013)
Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, et al. (eds.) [10], pp. 131–153
Mencía, C., Previti, A., Marques-Silva, J.: Literal-based MCS extraction. In: IJCAI (2015)
Morgado, A., Liffiton, M., Marques-Silva, J.: MaxSAT-based MCS enumeration. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 86–101. Springer, Heidelberg (2013)
Murakami, K., Uno, T.: Efficient algorithms for dualizing large-scale hypergraphs. CoRR, abs/1102.3813 (2011)
Nadel, A., Ryvchin, V., Strichman, O.: Efficient MUS extraction with resolution. In: FMCAD, pp. 197–200 (2013)
Rector, A.L., Horrocks, I.R.: Experience building a large, re-usable medical ontology using a description logic with transitivity and concept inclusions. In: Workshop on Ontological Engineering, pp. 414–418 (1997)
Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)
Schlobach, S., Huang, Z., Cornet, R., van Harmelen, F.: Debugging incoherent terminologies. J. Autom. Reasoning 39(3), 317–349 (2007)
Sebastiani, R., Vescovi, M.: Axiom pinpointing in lightweight description logics via horn-SAT encoding and conflict analysis. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 84–99. Springer, Heidelberg (2009)
Sebastiani, R., Vescovi, M.: Axiom pinpointing in large \({\cal EL}^+\) ontologies via SAT and SMT techniques. Technical Report DISI-15-010, DISI, University of Trento, Italy, April 2015. http://disi.unitn.it/rseba/elsat/elsat_techrep.pdf
Sioutos, N., de Coronado, S., Haber, M.W., Hartel, F.W., Shaiu, W.-L., Wright, L.W.: NCI thesaurus: A semantic model integrating cancer-related clinical and molecular information. Journal of Biomedical Informatics 40(1), 30–43 (2007)
Spackman, K.A., Campbell, K.E., Côté, R.A.: SNOMED RT: a reference terminology for health care. In: AMIA (1997)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Arif, M.F., Mencía, C., Marques-Silva, J. (2015). Efficient Axiom Pinpointing with EL2MCS. In: Hölldobler, S., , Peñaloza, R., Rudolph, S. (eds) KI 2015: Advances in Artificial Intelligence. KI 2015. Lecture Notes in Computer Science(), vol 9324. Springer, Cham. https://doi.org/10.1007/978-3-319-24489-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-24489-1_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24488-4
Online ISBN: 978-3-319-24489-1
eBook Packages: Computer ScienceComputer Science (R0)