{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,19]],"date-time":"2024-05-19T21:10:13Z","timestamp":1716153013020},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,8,8]],"date-time":"2022-08-08T00:00:00Z","timestamp":1659916800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,8,8]],"date-time":"2022-08-08T00:00:00Z","timestamp":1659916800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2023,4]]},"DOI":"10.1007\/s11704-022-1360-x","type":"journal-article","created":{"date-parts":[[2022,8,8]],"date-time":"2022-08-08T12:03:21Z","timestamp":1659960201000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Lightweight axiom pinpointing via replicated driver and customized SAT-solving"],"prefix":"10.1007","volume":"17","author":[{"given":"Dantong","family":"Ouyang","sequence":"first","affiliation":[]},{"given":"Mengting","family":"Liao","sequence":"additional","affiliation":[]},{"given":"Yuxin","family":"Ye","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,8]]},"reference":[{"key":"1360_CR1","doi-asserted-by":"crossref","unstructured":"Baader F, Calvanese D, Mcguinness D L, et al. The Description Logic Handbook. Cambridge University Press, 2007","DOI":"10.1017\/CBO9780511711787"},{"key":"1360_CR2","doi-asserted-by":"crossref","unstructured":"Baader F, Pe\u00f1aloza R, Suntisrivaraporn B. Pinpointing in the description logic $${\\cal E}{{\\cal L}^ + }$$. In: Proceedings of the 30th Annual German Conference on Artificial Intelligence. 2007, 52\u201367","DOI":"10.1007\/978-3-540-74565-5_7"},{"key":"1360_CR3","unstructured":"Baader F, Suntisrivaraporn B. Debugging snomed CT using axiom pinpointing in the description logic $${\\cal E}{{\\cal L}^ + }$$. In: Proceedings of the 3rd International Conference on Knowledge Representation in Medicine. 2008, 1"},{"key":"1360_CR4","doi-asserted-by":"crossref","unstructured":"Suntisrivaraporn B, Baader F, Schulz S, Spackman K. Replacing SEP-Triplets in SNOMED CT using tractable description logic operators. In: Proceedings of the 11th Conference on Artificial Intelligence in Medicine. 2007, 287\u2013291","DOI":"10.1007\/978-3-540-73599-1_38"},{"key":"1360_CR5","unstructured":"Baader F, Brandt S, Lutz C. Pushing the $${\\cal E}{\\cal L}$$ envelope. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence. 2005, 364\u2013369"},{"key":"1360_CR6","doi-asserted-by":"crossref","unstructured":"Sebastiani R, Vescovi M. Axiom pinpointing in lightweight description logics via horn-sat encoding and conflict analysis. In: Proceedings of the 22nd International Conference on Automated Deduction. 2009, 84\u201399","DOI":"10.1007\/978-3-642-02959-2_6"},{"key":"1360_CR7","doi-asserted-by":"crossref","unstructured":"Arif M F, Menc\u00eda C, Marques-Silva J. Efficient axiom pinpointing with EL2MCS. In: Proceedings of the 38th Annual German Conference on Artificial Intelligence. 2015, 225\u2013233","DOI":"10.1007\/978-3-319-24489-1_17"},{"key":"1360_CR8","doi-asserted-by":"crossref","unstructured":"Arif M F, Menc\u00eda C, Marques-Silva J. Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing. In: Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing. 2015, 324\u2013342","DOI":"10.1007\/978-3-319-24318-4_24"},{"key":"1360_CR9","unstructured":"Manthey N, Pe\u00f1aloza R, Rudolph S. Efficient axiom pinpointing in $${\\cal E}{\\cal L}$$ using SAT technology. In: Proceedings of the 29th International Workshop on Description Logics. 2016"},{"key":"1360_CR10","doi-asserted-by":"crossref","unstructured":"Arif M F, Menc\u00eda C, Ignatiev A, Manthey N, Pe\u00f1aloza R, Marques-Silva J. BEACON: an efficient SAT-based tool for debugging $${\\cal E}{{\\cal L}^ + }$$ ontologies. In: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing. 2016, 521\u2013530","DOI":"10.1007\/978-3-319-40970-2_32"},{"key":"1360_CR11","unstructured":"Ignatiev A, Marques-Silva J, Menc\u00eda C, Pe\u00f1aloza R. Debugging $${\\cal E}{{\\cal L}^ + }$$ ontologies through horn MUS enumeration. In: Proceedings of the 30th International Workshop on Description Logics. 2017, 1"},{"key":"1360_CR12","doi-asserted-by":"crossref","unstructured":"Kazakov Y, Sko\u010dovsk\u00fd P. Enumerating justifications using resolution. In: Proceedings of the 9th International Joint Conference on Automated Reasoning. 2018, 609\u2013626","DOI":"10.1007\/978-3-319-94205-6_40"},{"key":"1360_CR13","doi-asserted-by":"crossref","unstructured":"Gao M, Ye Y, Ouyang D, Wang B. Finding justifications by approximating core for large-scale ontologies. In: Proceedings of the 28th International Joint Conference on Artificial Intelligence. 2019, 6432\u20136433","DOI":"10.24963\/ijcai.2019\/905"},{"issue":"3","key":"1360_CR14","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s13218-020-00669-4","volume":"34","author":"N Manthey","year":"2020","unstructured":"Manthey N, Pe\u00f1aloza R, Rudolph S. SATPIN: Axiom pinpointing for lightweight description logics through incremental SAT. KI-K\u00fcnstliche Intelligenz, 2020, 34(3): 389\u2013394","journal-title":"KI-K\u00fcnstliche Intelligenz"},{"issue":"4","key":"1360_CR15","doi-asserted-by":"publisher","first-page":"144305","DOI":"10.1007\/s11704-019-7267-5","volume":"14","author":"Y Ye","year":"2020","unstructured":"Ye Y, Cui X, Ouyang D. Extracting a justification for OWL ontologies by critical axioms. Frontiers of Computer Science, 2020, 14(4): 144305","journal-title":"Frontiers of Computer Science"},{"issue":"2","key":"1360_CR16","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/s10489-019-01528-y","volume":"50","author":"J Gao","year":"2020","unstructured":"Gao J, Ouyang D T, Ye Y. Exploring duality on ontology debugging. Applied Intelligence, 2020, 50(2): 620\u2013633","journal-title":"Applied Intelligence"},{"key":"1360_CR17","unstructured":"S\u00f6rensson N, Een N. MiniSat v1.13- A SAT solver with conflict-clause minimization. In: Proceedings of the 8th Conference on Theory and Applications of Satisfiability Testing. 2005, 502\u2013518"},{"issue":"1","key":"1360_CR18","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. Information Processing Letters, 1988, 29(1): 1\u201312","journal-title":"Information Processing Letters"},{"key":"1360_CR19","unstructured":"Baader F, Lutz C, Suntisrivaraporn B. Efficient reasoning in $${\\cal E}{{\\cal L}^ + }$$. In: Proceedings of the 2006 International Workshop on Description Logics. 2006, 15"},{"key":"1360_CR20","doi-asserted-by":"crossref","unstructured":"Bailey J, Stuckey P J. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages. 2005, 174\u2013186","DOI":"10.1007\/978-3-540-30557-6_14"},{"key":"1360_CR21","unstructured":"Bend\u00edk J, Benes N, Cern\u00e1 I, Barnat J. Tunable online MUS\/MSS enumeration. In: Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. 2016, 50: 1\u201350: 13"},{"key":"1360_CR22","doi-asserted-by":"crossref","unstructured":"Narodytska N, Bj\u00f8rner N, Marinescu M C, Sagiv M. Core-guided minimal correction set and core enumeration. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence. 2018, 1353\u20131361","DOI":"10.24963\/ijcai.2018\/188"},{"key":"1360_CR23","doi-asserted-by":"crossref","unstructured":"Bend\u00edk J, \u010cern\u00e1 I, Bene\u0161 N. Recursive online enumeration of all minimal unsatisfiable subsets. In: Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis. 2018, 143\u2013159","DOI":"10.1007\/978-3-030-01090-4_9"},{"key":"1360_CR24","doi-asserted-by":"crossref","unstructured":"Bend\u00edk J, \u010cern\u00e1 I. Replication-guided enumeration of minimal unsatisfiable subsets. In: Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming. 2020, 37\u201354","DOI":"10.1007\/978-3-030-58475-7_3"},{"key":"1360_CR25","doi-asserted-by":"crossref","unstructured":"Bend\u00edk J, \u010cern\u00e1 I. MUST: Minimal unsatisfiable subsets enumeration tool. In: Proceedings of the 26th International Conferences on Tools and Algorithms for the Construction and Analysis of Systems. 2020, 135\u2013152","DOI":"10.1007\/978-3-030-45190-5_8"},{"key":"1360_CR26","doi-asserted-by":"crossref","unstructured":"Pe\u00f1aloza R, Sertkaya B. On the complexity of axiom pinpointing in the EL family of description logics. In: Proceedings of the 12th International Conference on Principles of Knowledge Representation and Reasoning. 2010, 280\u2013289","DOI":"10.25368\/2022.173"},{"key":"1360_CR27","doi-asserted-by":"crossref","unstructured":"Marques-Silva J, Ignatiev A, Menc\u00eda C, Pe\u00f1aloza R. Efficient reasoning for inconsistent horn formulae. In: Proceedings of the 15th European Conference on Logics in Artificial Intelligence. 2016, 336\u2013352","DOI":"10.1007\/978-3-319-48758-8_22"},{"issue":"3\u20134","key":"1360_CR28","doi-asserted-by":"publisher","first-page":"123","DOI":"10.3233\/SAT190094","volume":"8","author":"A Belov","year":"2012","unstructured":"Belov A, Marques-Silva J. MUSer2: an efficient MUS extractor. Journal on Satisfiability, Boolean Modeling and Computation, 2012, 8(3\u20134): 123\u2013128","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"1360_CR29","doi-asserted-by":"crossref","unstructured":"Bacchus F, Katsirelos G. Using minimal correction sets to more efficiently compute minimal unsatisfiable sets. In: Proceedings of the 27th International Conference on Computer Aided Verification. 2015, 70\u201386","DOI":"10.1007\/978-3-319-21668-3_5"},{"key":"1360_CR30","unstructured":"Kilby P, Slaney J, Thi\u00e9baux S, Walsh T. Backbones and backdoors in satisfiability. In: Proceedings of the 20th National Conference on Artificial Intelligence. 2005, 1368\u20131373"},{"key":"1360_CR31","unstructured":"Audemard G, Simon L. Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence. 2009, 399\u2013404"},{"key":"1360_CR32","doi-asserted-by":"crossref","unstructured":"Moskewicz M W, Madigan C F, Zhao Y, Zhang L, Malik S. Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference. 2001, 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"1360_CR33","doi-asserted-by":"crossref","unstructured":"Liang J H, Ganesh V, Zulkoski E, Zaman A, Czarnecki K. Understanding VSIDS branching heuristics in conflict-driven clause-learning SAT solvers. In: Proceedings of the 11th International Haifa Verification Conference on Hardware and Software: Verification and Testing. 2015, 225\u2013241","DOI":"10.1007\/978-3-319-26287-1_14"},{"key":"1360_CR34","doi-asserted-by":"crossref","unstructured":"Oh C. Between SAT and UNSAT: the fundamental difference in CDCL SAT. In: Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing. 2015, 307\u2013323","DOI":"10.1007\/978-3-319-24318-4_23"},{"key":"1360_CR35","doi-asserted-by":"crossref","unstructured":"Morgado A, Liffiton M, Marques-Silva J. MaxSAT-based MCS enumeration. In: Proceedings of the 8th International Haifa Verification Conference on Hardware and Software: Verification and Testing. 2012, 86\u2013101","DOI":"10.1007\/978-3-642-39611-3_13"},{"issue":"1","key":"1360_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"M H Liffiton","year":"2008","unstructured":"Liffiton M H, Sakallah K A. Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning, 2008, 40(1): 1\u201333","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"1360_CR37","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10601-015-9183-0","volume":"21","author":"M H Liffiton","year":"2016","unstructured":"Liffiton M H, Previti A, Malik A, Marques-Silva J. Fast, flexible MUS enumeration. Constraints, 2016, 21(2): 223\u2013250","journal-title":"Constraints"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-022-1360-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11704-022-1360-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-022-1360-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,19]],"date-time":"2024-05-19T20:35:34Z","timestamp":1716150934000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11704-022-1360-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,8]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4]]}},"alternative-id":["1360"],"URL":"https:\/\/doi.org\/10.1007\/s11704-022-1360-x","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,8]]},"assertion":[{"value":"11 July 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 December 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 August 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"172315"}}