{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T21:04:09Z","timestamp":1772831049357,"version":"3.50.1"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319243177","type":"print"},{"value":"9783319243184","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24318-4_24","type":"book-chapter","created":{"date-parts":[[2015,9,11]],"date-time":"2015-09-11T05:42:56Z","timestamp":1441950176000},"page":"324-342","source":"Crossref","is-referenced-by-count":14,"title":["Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing"],"prefix":"10.1007","author":[{"given":"M. Fareed","family":"Arif","sequence":"first","affiliation":[]},{"given":"Carlos","family":"Menc\u00eda","sequence":"additional","affiliation":[]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,27]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Arif, M.F., Menc\u00eda, C., Marques-Silva, J.: Efficient axiom pinpointing with EL2MCS. In: KI (2015)","DOI":"10.1007\/978-3-319-24489-1_17"},{"issue":"1","key":"24_CR2","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1038\/75556","volume":"25","author":"M Ashburner","year":"2000","unstructured":"Ashburner, M., Ball, C.A., Blake, J.A., Botstein, D., Butler, H., Cherry, J.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\u201329 (2000)","journal-title":"Nature genetics"},{"issue":"1","key":"24_CR3","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF00883932","volume":"14","author":"F Baader","year":"1995","unstructured":"Baader, F., Hollunder, B.: Embedding defaults into terminological knowledge representation formalisms. J. Autom. Reasoning 14(1), 149\u2013180 (1995)","journal-title":"J. Autom. Reasoning"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Baader, F., Horrocks, I., Sattler, U.; Description logics. In: van Harmelen, V.L.F., Porter, B. (eds.), Handbook of Knowledge Representation, Foundations of Artificial Intelligence, chapter 3, pp. 135\u2013179. Elsevier (2008)","DOI":"10.1016\/S1574-6526(07)03003-9"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/11814771_25","volume-title":"Automated Reasoning","author":"F Baader","year":"2006","unstructured":"Baader, F., Lutz, C., Suntisrivaraporn, B.: CEL \u2014 a polynomial-time reasoner for life science ontologies. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 287\u2013291. Springer, Heidelberg (2006)"},{"issue":"1","key":"24_CR6","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1093\/logcom\/exn058","volume":"20","author":"F Baader","year":"2010","unstructured":"Baader, F., Pe\u00f1aloza, R.: Axiom pinpointing in general tableaux. J. Log. Comput. 20(1), 5\u201334 (2010)","journal-title":"J. Log. Comput."},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Baader, F., Pe\u00f1aloza, R., Suntisrivaraporn, B.: Pinpointing in the description logic $${\\cal EL}^{+}$$ . In: KI, pp. 52\u201367 (2007)","DOI":"10.1007\/978-3-540-74565-5_7"},{"key":"24_CR8","unstructured":"Baader, F., Suntisrivaraporn, B.: Debugging SNOMED CT using axiom pinpointing in the description logic $${\\cal EL}^{+}$$ . In: KR-MED (2008)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Bacchus, F., Davies, J., Tsimpoukelli, M., Katsirelos, G.: Relaxation search: a simple way of managing optional clauses. In: AAAI, pp. 835\u2013841 (2014)","DOI":"10.1609\/aaai.v28i1.8849"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-540-30557-6_14","volume-title":"Practical Aspects of Declarative Languages","author":"J Bailey","year":"2005","unstructured":"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\u2013186. Springer, Heidelberg (2005)"},{"key":"24_CR11","unstructured":"Bakker, R.R., Dikker, F., Tempelman, F., Wognum, P.M.: Diagnosing and solving over-determined constraint satisfaction problems. In: IJCAI, pp. 276\u2013281 (1993)"},{"issue":"2","key":"24_CR12","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/AIC-2012-0523","volume":"25","author":"A Belov","year":"2012","unstructured":"Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"key":"24_CR13","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)"},{"issue":"1","key":"24_CR14","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1080\/0952813021000026795","volume":"15","author":"E Birnbaum","year":"2003","unstructured":"Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15(1), 25\u201346 (2003)","journal-title":"J. Exp. Theor. Artif. Intell."},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: STOC, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"key":"24_CR16","unstructured":"de Siqueira, N.J.L., Puget, J.-F.: Explanation-based generalisation of failures. In: ECAI, pp. 339\u2013344 (1988)"},{"issue":"3","key":"24_CR17","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"WF Dowling","year":"1984","unstructured":"Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 1(3), 267\u2013284 (1984)","journal-title":"J. Log. Program."},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"24_CR19","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1613\/jair.4016","volume":"48","author":"I Gent","year":"2013","unstructured":"Gent, I.: Optimal implementation of watched literals and more general techniques. Journal of Artificial Intelligence Research 48, 231\u2013252 (2013)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"24_CR20","unstructured":"Giunchiglia, E., Maratea, M.: Solving optimization problems with DLL. In: ECAI, pp. 377\u2013381 (2006)"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, \u00c9., Lagniez, J., Mazure, B.: An experimentally efficient method for (MSS, CoMSS) partitioning. In: AAAI, pp. 2666\u20132673 (2014)","DOI":"10.1609\/aaai.v28i1.9118"},{"issue":"2","key":"24_CR22","doi-asserted-by":"crossref","first-page":"195","DOI":"10.3233\/AIC-140636","volume":"28","author":"F Heras","year":"2015","unstructured":"Heras, F., Morgado, A., Marques-Silva, J.: MaxSAT-based encodings for group MaxSAT. AI Commun. 28(2), 195\u2013214 (2015)","journal-title":"AI Commun."},{"issue":"2","key":"24_CR23","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0743-1066(87)90014-8","volume":"4","author":"A Itai","year":"1987","unstructured":"Itai, A., Makowsky, J.A.: Unification as a complexity measure for logic programming. J. Log. Program. 4(2), 105\u2013117 (1987)","journal-title":"J. Log. Program."},{"key":"24_CR24","unstructured":"Junker, U.: QuickXplain: preferred explanations and relaxations for over-constrained problems. In: AAAI, pp. 167\u2013172 (2004)"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/978-3-540-76298-0_20","volume-title":"The Semantic Web","author":"A Kalyanpur","year":"2007","unstructured":"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.J.B., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., Cudr\u00e9-Mauroux, P. (eds.) ASWC 2007 and ISWC 2007. LNCS, vol. 4825, pp. 267\u2013280. Springer, Heidelberg (2007)"},{"key":"24_CR26","series-title":"lecture notes in computer science","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1007\/11762256_15","volume-title":"The Semantic Web: Research and Applications","author":"A Kalyanpur","year":"2006","unstructured":"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\u2013184. Springer, Heidelberg (2006)"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1007\/11817963_39","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2006","unstructured":"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\u2013437. Springer, Heidelberg (2006)"},{"key":"24_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/978-3-642-38171-3_11","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"MH Liffiton","year":"2013","unstructured":"Liffiton, M.H., Malik, A.: Enumerating infeasibility: finding multiple MUSes quickly. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 160\u2013175. Springer, Heidelberg (2013)"},{"key":"24_CR29","unstructured":"Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints (2015). http:\/\/link.springer.com\/article\/10.1007\/s10601-015-9183-0"},{"issue":"1","key":"24_CR30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1\u201333 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"24_CR31","unstructured":"Ludwig, M.: Just: a tool for computing justifications w.r.t. ELH ontologies. In: ORE (2014)"},{"key":"24_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/978-3-319-11558-0_8","volume-title":"Logics in Artificial Intelligence","author":"M Ludwig","year":"2014","unstructured":"Ludwig, M., Pe\u00f1aloza, R.: Error-tolerant reasoning in the description logic $${\\cal EL}$$ . In: Ferm\u00e9, E., Leite, J. (eds.) JELIA 2014. LNCS, vol. 8761, pp. 107\u2013121. Springer, Heidelberg (2014)"},{"key":"24_CR33","unstructured":"Manthey, N., Pe\u00f1aloza, R.: Exploiting SAT technology for axiom pinpointing. Technical Report LTCS 15\u201305, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit\u00e4t Dresden, April 2015. https:\/\/ddll.inf.tu-dresden.de\/web\/Techreport3010"},{"key":"24_CR34","unstructured":"Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI, pp. 615\u2013622 (2013)"},{"key":"24_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"592","DOI":"10.1007\/978-3-642-39799-8_39","volume-title":"Computer Aided Verification","author":"J Marques-Silva","year":"2013","unstructured":"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\u2013607. Springer, Heidelberg (2013)"},{"key":"24_CR36","unstructured":"Menc\u00eda, C., Previti, A., Marques-Silva, J.: Literal-based MCS extraction. In: IJCAI, pp. 1973\u20131979 (2015)"},{"key":"24_CR37","unstructured":"Meyer, T.A., Lee, K., Booth, R., Pan, J.Z.: Finding maximally satisfiable terminologies for the description logic $${\\cal EL}^+$$ . In: AAAI, pp. 269\u2013274 (2006)"},{"issue":"1","key":"24_CR38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0020-0190(88)90124-X","volume":"29","author":"M Minoux","year":"1988","unstructured":"Minoux, M.: LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation. Inf. Process. Lett. 29(1), 1\u201312 (1988)","journal-title":"Inf. Process. Lett."},{"key":"24_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/978-3-642-23580-1_24","volume-title":"Web Reasoning and Rule Systems","author":"K Moodley","year":"2011","unstructured":"Moodley, K., Meyer, T., Varzinczak, I.J.: Root justifications for ontology repair. In: Rudolph, S., Gutierrez, C. (eds.) RR 2011. LNCS, vol. 6902, pp. 275\u2013280. Springer, Heidelberg (2011)"},{"key":"24_CR40","unstructured":"Nguyen, H.H., Alechina, N., Logan, B.: Axiom pinpointing using an assumption-based truth maintenance system. In: DL (2012)"},{"key":"24_CR41","unstructured":"O\u2019Sullivan, B., Papadopoulos, A., Faltings, B., Pu, P.: Representative explanations for over-constrained problems. In: AAAI, pp. 323\u2013328 (2007)"},{"key":"24_CR42","doi-asserted-by":"crossref","unstructured":"Parsia, B., Sirin, E., Kalyanpur, A.; Debugging OWL ontologies. In: WWW, pp. 633\u2013640 (2005)","DOI":"10.1145\/1060745.1060837"},{"key":"24_CR43","doi-asserted-by":"crossref","unstructured":"Pe\u00f1aloza, R., Sertkaya, B.: On the complexity of axiom pinpointing in the EL family of description logics. In: KR (2010)","DOI":"10.25368\/2022.173"},{"key":"24_CR44","doi-asserted-by":"crossref","unstructured":"Previti, A., Marques-Silva, J.: Partial MUS enumeration. In: AAAI, pp. 818\u2013825 (2013)","DOI":"10.1609\/aaai.v27i1.8657"},{"key":"24_CR45","unstructured":"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\u2013418 (1997)"},{"issue":"1","key":"24_CR46","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R Reiter","year":"1987","unstructured":"Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57\u201395 (1987)","journal-title":"Artif. Intell."},{"issue":"4","key":"24_CR47","doi-asserted-by":"crossref","first-page":"395","DOI":"10.3233\/AIC-130575","volume":"26","author":"ED Rosa","year":"2013","unstructured":"Rosa, E.D., Giunchiglia, E.: Combining approaches for solving satisfiability problems with qualitative preferences. AI Commun. 26(4), 395\u2013408 (2013)","journal-title":"AI Commun."},{"key":"24_CR48","unstructured":"Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: IJCAI, pp. 355\u2013362 (2003)"},{"issue":"3","key":"24_CR49","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/s10817-007-9076-z","volume":"39","author":"S Schlobach","year":"2007","unstructured":"Schlobach, S., Huang, Z., Cornet, R., van Harmelen, F.: Debugging incoherent terminologies. J. Autom. Reasoning 39(3), 317\u2013349 (2007)","journal-title":"J. Autom. Reasoning"},{"key":"24_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/978-3-642-02959-2_6","volume-title":"Automated Deduction \u2013 CADE-22","author":"R Sebastiani","year":"2009","unstructured":"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\u201399. Springer, Heidelberg (2009)"},{"key":"24_CR51","unstructured":"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. Under Journal Submission. http:\/\/disi.unitn.it\/ rseba\/elsat\/elsat_techrep.pdf"},{"issue":"1","key":"24_CR52","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1016\/j.jbi.2006.02.013","volume":"40","author":"N Sioutos","year":"2007","unstructured":"Sioutos, N., de Coronado, S., Haber, M.W., Hartel, F.W., Shaiu, W., Wright, L.W.: NCI thesaurus: A semantic model integrating cancer-related clinical and molecular information. Journal of Biomedical Informatics 40(1), 30\u201343 (2007)","journal-title":"Journal of Biomedical Informatics"},{"issue":"2","key":"24_CR53","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/j.websem.2007.03.004","volume":"5","author":"E Sirin","year":"2007","unstructured":"Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: A practical OWL-DL reasoner. J. Web Sem. 5(2), 51\u201353 (2007)","journal-title":"J. Web Sem."},{"key":"24_CR54","doi-asserted-by":"crossref","unstructured":"Slaney, J.: Set-theoretic duality: a fundamental feature of combinatorial optimisation. In: ECAI, pp. 843\u2013848 (2014)","DOI":"10.3233\/978-1-61499-419-0-843"},{"key":"24_CR55","unstructured":"Spackman, K.A., Campbell, K.E., C\u00f4t\u00e9, R.A.: SNOMED RT: a reference terminology for health care. In: AMIA (1997)"},{"key":"24_CR56","unstructured":"Vescovi, M.: Exploiting SAT and SMT Techniques for Automated Reasoning and Ontology Manipulation in Description Logics. Ph.D. thesis, University of Trento (2011)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing -- SAT 2015"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24318-4_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T15:26:48Z","timestamp":1748618808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24318-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243177","9783319243184"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24318-4_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}