{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T22:00:11Z","timestamp":1790546411866,"version":"4.1.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319409696","type":"print"},{"value":"9783319409702","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_32","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T11:14:55Z","timestamp":1465557295000},"page":"521-530","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["BEACON: An Efficient SAT-Based Tool for Debugging $${\\mathcal {EL}}{^+}$$ Ontologies"],"prefix":"10.1007","author":[{"given":"M. Fareed","family":"Arif","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carlos","family":"Menc\u00eda","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexey","family":"Ignatiev","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Norbert","family":"Manthey","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rafael","family":"Pe\u00f1aloza","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-319-24489-1_17","volume-title":"KI 2015: Advances in Artificial Intelligence","author":"MF Arif","year":"2015","unstructured":"Arif, M.F., Menc\u00eda, C., Marques-Silva, J.: Efficient axiom pinpointing with EL2MCS. In: H\u00f6lldobler, S., Kr\u00f6tzsch, M., Pe\u00f1aloza, R., Rudolph, S., Edelkamp, S., Edelkamp, S. (eds.) KI 2015. LNCS, vol. 9324, pp. 225\u2013233. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-24489-1_17"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-319-24318-4_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"MF Arif","year":"2015","unstructured":"Arif, M.F., Menc\u00eda, C., Marques-Silva, J.: Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 324\u2013342. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-24318-4_24"},{"issue":"1","key":"32_CR3","doi-asserted-by":"publisher","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. Nat. Genet. 25(1), 25\u201329 (2000)","journal-title":"Nat. Genet."},{"key":"32_CR4","unstructured":"Baader, F., Brandt, S., Lutz, C.: Pushing the $${\\cal EL}$$ envelope. In: IJCAI, pp. 364\u2013369 (2005)"},{"key":"32_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11814771_25","volume-title":"Automated Reasoning","author":"F Baader","year":"2006","unstructured":"Baader, F., Lutz, C., Suntisrivaraporn, B.: $$\\sf {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)"},{"key":"32_CR6","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":"32_CR7","unstructured":"Baader, F., Suntisrivaraporn, B.: Debugging SNOMED CT using axiom pinpointing in the description logic $${\\cal EL{^+}}$$ . In: KR-MED (2008)"},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"32_CR9","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"issue":"1","key":"32_CR10","doi-asserted-by":"publisher","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":"32_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-23786-7_19","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"J Davies","year":"2011","unstructured":"Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 225\u2013239. Springer, Heidelberg (2011)"},{"issue":"3","key":"32_CR12","doi-asserted-by":"publisher","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":"32_CR13","unstructured":"Gupta, A.: Learning Abstractions for Model Checking. Ph.D. thesis, Carnegie Mellon University, June 2006"},{"key":"32_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-319-23219-5_13","volume-title":"Principles and Practice of Constraint Programming","author":"A Ignatiev","year":"2015","unstructured":"Ignatiev, A., Previti, A., Liffiton, M., Marques-Silva, J.: Smallest MUS extraction with minimal hitting set dualization. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 173\u2013182. Springer, Heidelberg (2015)"},{"issue":"2","key":"32_CR15","doi-asserted-by":"publisher","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."},{"issue":"2","key":"32_CR16","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.artint.2004.11.002","volume":"163","author":"P Liberatore","year":"2005","unstructured":"Liberatore, P.: Redundancy in logic I: CNF propositional formulae. Artif. Intell. 163(2), 203\u2013232 (2005)","journal-title":"Artif. Intell."},{"key":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"32_CR18","unstructured":"Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUs enumeration. Constraints (2015). Online version: http:\/\/link.springer.com\/article\/10.1007\/s10601-015-9183-0"},{"issue":"1","key":"32_CR19","doi-asserted-by":"publisher","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":"32_CR20","unstructured":"Ludwig, M.: Just: a tool for computing justifications w.r.t. ELH ontologies. In: ORE (2014)"},{"key":"32_CR21","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":"32_CR22","unstructured":"Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI, pp. 615\u2013622 (2013)"},{"key":"32_CR23","unstructured":"Menc\u00eda, C., Previti, A., Marques-Silva, J.: Literal-based MCS extraction. In: IJCAI, pp. 1973\u20131979 (2015)"},{"issue":"1","key":"32_CR24","doi-asserted-by":"publisher","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":"32_CR25","doi-asserted-by":"crossref","unstructured":"Pe\u00f1aoza, R.: Axiom pinpointing in description logics and beyond. Ph.D. thesis, Dresden University of Technology (2009)","DOI":"10.25368\/2022.173"},{"key":"32_CR26","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":"32_CR27","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":"32_CR28","doi-asserted-by":"publisher","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."},{"key":"32_CR29","unstructured":"Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: IJCAI, pp. 355\u2013362 (2003)"},{"key":"32_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"32_CR31","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, Under Journal Submission, April 2015. http:\/\/disi.unitn.it\/~rseba\/elsat\/elsat_techrep.pdf"},{"issue":"1","key":"32_CR32","doi-asserted-by":"publisher","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. J. Biomed. Inform. 40(1), 30\u201343 (2007)","journal-title":"J. Biomed. Inform."},{"key":"32_CR33","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":"32_CR34","unstructured":"Spackman, K.A., Campbell, K.E., C\u00f4t\u00e9, R.A.: SNOMED RT: a reference terminology for health care. In: AMIA (1997)"},{"key":"32_CR35","first-page":"111","volume":"6","author":"S Stefan","year":"2011","unstructured":"Stefan, S., Ronald, C., Spackman, K.A.: Consolidating SNOMED CT\u2019s ontological commitment. Appl. Ontol. 6, 111 (2011)","journal-title":"Appl. Ontol."}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T21:19:19Z","timestamp":1748985559000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"11 June 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}