{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T17:20:04Z","timestamp":1740158404741,"version":"3.37.3"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,6,2]],"date-time":"2020-06-02T00:00:00Z","timestamp":1591056000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,6,2]],"date-time":"2020-06-02T00:00:00Z","timestamp":1591056000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["Consolidator Grant 771779"],"award-info":[{"award-number":["Consolidator Grant 771779"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["K\u00fcnstl Intell"],"published-print":{"date-parts":[[2020,9]]},"DOI":"10.1007\/s13218-020-00669-4","type":"journal-article","created":{"date-parts":[[2020,6,3]],"date-time":"2020-06-03T16:45:31Z","timestamp":1591202731000},"page":"389-394","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["SATPin: Axiom Pinpointing for Lightweight Description Logics Through Incremental SAT"],"prefix":"10.1007","volume":"34","author":[{"given":"Norbert","family":"Manthey","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2693-5790","authenticated-orcid":false,"given":"Rafael","family":"Pe\u00f1aloza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Rudolph","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,2]]},"reference":[{"key":"669_CR1","doi-asserted-by":"crossref","unstructured":"Arif MF, Menc\u00eda C, Ignatiev A, Manthey N, Pe\u00f1aloza R, Marques-Silva J (2016) BEACON: an efficient sat-based tool for debugging EL+ ontologies. In: Proc. of SAT 2016, LNCS, vol 9710. Springer, pp 521\u2013530","DOI":"10.1007\/978-3-319-40970-2_32"},{"key":"669_CR2","unstructured":"Baader F, Suntisrivaraporn B (2008) Debugging SNOMED CT using axiom pinpointing in the description logic $${\\cal{EL}}^{+}$$. In: Proc. of KR-MED\u201908, CEUR-WS, vol 410"},{"key":"669_CR3","unstructured":"Baader F, Brandt S, Lutz C (2005) Pushing the $${\\cal{EL}}$$ envelope. In: Proc. IJCAI-05. Morgan-Kaufmann"},{"key":"669_CR4","unstructured":"Baader F, Schulz S, Spackmann K, Suntisrivaraporn B (2009) How should parthood relations be expressed in SNOMED CT? In: Proc. of OBML 2009"},{"key":"669_CR5","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1016\/j.websem.2011.11.006","volume":"12\u201313","author":"F Baader","year":"2012","unstructured":"Baader F, Knechtel M, Pe\u00f1aloza R (2012) Context-dependent views to axioms and consequences of semantic web ontologies. J Web Semant 12\u201313:22\u201340","journal-title":"J Web Semant"},{"key":"669_CR6","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/j.artint.2016.08.007","volume":"241","author":"T Balyo","year":"2016","unstructured":"Balyo T, Biere A, Iser M, Sinz C (2016) SAT race 2015. Artif Intell 241:45\u201365","journal-title":"Artif Intell"},{"key":"669_CR7","doi-asserted-by":"crossref","unstructured":"Ceylan II, Pe\u00f1aloza R (2014) The Bayesian description logic $${\\cal{BEL}}$$. In: Proc. of IJCAR\u201914, LNCS, vol 8562. Springer, pp 480\u2013494","DOI":"10.1007\/978-3-319-08587-6_37"},{"key":"669_CR8","doi-asserted-by":"crossref","unstructured":"Kazakov Y, Skocovsk\u00fd P (2018) Enumerating justifications using resolution. In: Proc. of IJCAR 2018, LNCS, vol 10900. Springer, pp 609\u2013626","DOI":"10.1007\/978-3-319-94205-6_40"},{"key":"669_CR9","doi-asserted-by":"crossref","unstructured":"Liffiton MH, Malik A (2013) Enumerating infeasibility: finding multiple MUSes quickly. In: Integration of AI and OR techniques in constraint programming for combinatorial optimization problems, LNCS, vol 7874. Springer, pp 160\u2013175","DOI":"10.1007\/978-3-642-38171-3_11"},{"key":"669_CR10","doi-asserted-by":"crossref","unstructured":"Ludwig M, Pe\u00f1aloza R (2014) Error-tolerant reasoning in the description logic el. In: Proc. of JELIA\u201914, LNAI, vol 8761. Springer, pp 107\u2013121","DOI":"10.1007\/978-3-319-11558-0_8"},{"key":"669_CR11","unstructured":"Manthey N (2014) Riss 4.27. In: Proc. of SAT Comp. 2014, University of Helsinki, Department of CS Series of Publications B, vol B-2014-2, pp 65\u201367"},{"key":"669_CR12","unstructured":"Manthey N (2015) Refining unsatisfiable cores in incremental SAT solving. Tech. rep, TU Dresden"},{"key":"669_CR13","unstructured":"Manthey N, Pe\u00f1aloza R, Rudolph S (2016) Efficient axiom pinpointing in EL using SAT technology. In: Proc. of DL 2016, CEUR Ws, vol 1577"},{"key":"669_CR14","doi-asserted-by":"crossref","unstructured":"Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proc. DAC 2001. ACM, pp 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"669_CR15","doi-asserted-by":"crossref","unstructured":"Pe\u00f1aloza R, Menc\u00eda C, Ignatiev A, Marques-Silva J (2017) Lean kernels in description logics. In: Proc. ESWC 2017, LNCS, vol 10249. Springer, pp 518\u2013533","DOI":"10.1007\/978-3-319-58068-5_32"},{"key":"669_CR16","doi-asserted-by":"crossref","unstructured":"Previti A, Marques-Silva J (2013) Partial MUS enumeration. In: Proc. of 27th AAAI. AAAI Press","DOI":"10.1609\/aaai.v27i1.8657"},{"key":"669_CR17","doi-asserted-by":"crossref","unstructured":"Riguzzi F, Bellodi E, Lamma E, Zese R (2015) Probabilistic description logics under the distribution semantics. SWJ","DOI":"10.3233\/SW-140154"},{"key":"669_CR18","doi-asserted-by":"crossref","unstructured":"Schenk S, Dividino R, Staab S (2009) Reasoning with provenance, trust and all that other meta knowledge in OWL. In: SWPM, CEUR-WS.org, CEUR, vol 526","DOI":"10.2139\/ssrn.3199429"},{"key":"669_CR19","doi-asserted-by":"crossref","unstructured":"Sebastiani R, Vescovi M (2009) Axiom pinpointing in lightweight description logics via Horn-SAT encoding and conflict analysis. In: Proc. of 22nd CADE, LNCS, vol 5663. Springer, pp 84\u201399","DOI":"10.1007\/978-3-642-02959-2_6"},{"key":"669_CR20","unstructured":"Sebastiani R, Vescovi M (2015) Axiom pinpointing in large $$\\cal EL\\it +$$ ontologies via SAT and SMT techniques. Tech. Rep. DISI-15-010, University of Trento, Italy"},{"issue":"4","key":"669_CR21","first-page":"133","volume":"7","author":"P van der Tak","year":"2011","unstructured":"van der Tak P, Ramos A, Heule M (2011) Reusing the assignment trail in CDCL solvers. JSAT 7(4):133\u2013138","journal-title":"JSAT"}],"container-title":["KI - K\u00fcnstliche Intelligenz"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13218-020-00669-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s13218-020-00669-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13218-020-00669-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,26]],"date-time":"2022-10-26T11:53:16Z","timestamp":1666785196000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s13218-020-00669-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,2]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,9]]}},"alternative-id":["669"],"URL":"https:\/\/doi.org\/10.1007\/s13218-020-00669-4","relation":{},"ISSN":["0933-1875","1610-1987"],"issn-type":[{"type":"print","value":"0933-1875"},{"type":"electronic","value":"1610-1987"}],"subject":[],"published":{"date-parts":[[2020,6,2]]},"assertion":[{"value":"29 November 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 May 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 June 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}