{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T23:24:42Z","timestamp":1742945082361,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319537320"},{"type":"electronic","value":"9783319537337"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-53733-7_7","type":"book-chapter","created":{"date-parts":[[2017,2,15]],"date-time":"2017-02-15T10:39:21Z","timestamp":1487155161000},"page":"103-114","source":"Crossref","is-referenced-by-count":1,"title":["An Automata View to Goal-Directed Methods"],"prefix":"10.1007","author":[{"given":"Lisa","family":"Hutschenreiter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rafael","family":"Pe\u00f1aloza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,16]]},"reference":[{"key":"7_CR1","unstructured":"Baader, F., Brandt, S., Lutz, C.: Pushing the $$\\cal{EL}$$ envelope. In: Proceedings of IJCAI 2005. Morgan Kaufmann, Edinburgh (2005)"},{"issue":"9\u201310","key":"7_CR2","doi-asserted-by":"crossref","first-page":"1045","DOI":"10.1016\/j.ic.2008.03.006","volume":"206","author":"F Baader","year":"2008","unstructured":"Baader, F., Hladik, J., Pe\u00f1aloza, R.: Automata can show PSPACE results for description logics. Inf. Comput. 206(9\u201310), 1045\u20131056 (2008)","journal-title":"Inf. Comput."},{"key":"7_CR3","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.: Context-dependent views to axioms and consequences of semantic web ontologies. J. Web Semant. 12\u201313, 22\u201340 (2012)","journal-title":"J. Web Semant."},{"issue":"2","key":"7_CR4","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/s10817-010-9181-2","volume":"45","author":"F Baader","year":"2010","unstructured":"Baader, F., Pe\u00f1aloza, R.: Automata-based axiom pinpointing. J. Autom. Reason. 45(2), 91\u2013129 (2010)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"7_CR5","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":"7_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-74565-5_7","volume-title":"KI 2007: Advances in Artificial Intelligence","author":"F Baader","year":"2007","unstructured":"Baader, F., Pe\u00f1aloza, 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\u201367. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74565-5_7"},{"issue":"2","key":"7_CR7","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."},{"issue":"3","key":"7_CR8","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"issue":"2","key":"7_CR9","first-page":"24","volume":"23","author":"RQ Dividino","year":"2009","unstructured":"Dividino, R.Q., Schenk, S., Sizov, S., Staab, S.: Provenance, trust, explanations - and all that other meta knowledge. KI 23(2), 24\u201330 (2009)","journal-title":"KI"},{"issue":"1\u20132","key":"7_CR10","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/j.tcs.2007.02.055","volume":"380","author":"M Droste","year":"2007","unstructured":"Droste, M., Gastin, P.: Weighted automata and weighted logics. Theoret. Comput. Sci. 380(1\u20132), 69\u201386 (2007)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001). doi: 10.1007\/3-540-44585-4_6"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., et al. (eds.) ASWC\/ISWC -2007. LNCS, vol. 4825, pp. 267\u2013280. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-76298-0_20"},{"key":"7_CR13","unstructured":"Kazakov, Y.: Consequence-driven reasoning for Horn SHIQ ontologies. In: Boutilier, C. (ed.) Proceedings of IJCAI 2009, pp. 2040\u20132045 (2009)"},{"key":"7_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-013-9296-3","volume":"53","author":"Y Kazakov","year":"2014","unstructured":"Kazakov, Y., Kr\u00f6tzsch, M., Siman\u010d\u00edk, F.: The incredible ELK: from polynomial procedures to efficient reasoning with $$\\cal{E\\!L}$$ ontologies. J. Autom. Reason. 53, 1\u201361 (2014)","journal-title":"J. Autom. Reason."},{"key":"7_CR15","unstructured":"Kleine B\u00fcning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Handbook of Satisfiability, pp. 339\u2013401 (2009)"},{"issue":"1\u20133","key":"7_CR16","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/S0166-218X(00)00262-6","volume":"107","author":"O Kullmann","year":"2000","unstructured":"Kullmann, O.: Investigations on autark assignments. Discret. Appl. Math. 107(1\u20133), 99\u2013137 (2000)","journal-title":"Discret. Appl. Math."},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/11814948_4","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"O Kullmann","year":"2006","unstructured":"Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of clauses in conjunctive normal forms: minimally unsatisfiable sub-clause-sets and the lean kernel. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 22\u201335. Springer, Heidelberg (2006). doi: 10.1007\/11814948_4"},{"issue":"2","key":"7_CR18","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/s10601-015-9183-0","volume":"21","author":"MH Liffiton","year":"2016","unstructured":"Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223\u2013250 (2016)","journal-title":"Constraints"},{"issue":"4","key":"7_CR19","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1016\/j.ic.2006.08.009","volume":"205","author":"R Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557\u2013580 (2007)","journal-title":"Inf. Comput."},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-642-13089-2_41","volume-title":"Language and Automata Theory and Applications","author":"R Pe\u00f1aloza","year":"2010","unstructured":"Pe\u00f1aloza, R.: Using sums-of-products for non-standard reasoning. In: Dediu, A.-H., Fernau, H., Mart\u00edn-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 488\u2013499. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-13089-2_41"},{"issue":"5","key":"7_CR21","doi-asserted-by":"crossref","first-page":"477","DOI":"10.3233\/SW-140154","volume":"6","author":"F Riguzzi","year":"2015","unstructured":"Riguzzi, F., Bellodi, E., Lamma, E., Zese, R.: Probabilistic description logics under the distribution semantics. Semant. Web 6(5), 477\u2013501 (2015)","journal-title":"Semant. Web"},{"key":"7_CR22","unstructured":"Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: Proceedings of IJCAI 2003, pp. 355\u2013362. Morgan Kaufmann (2003)"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-53733-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,2]],"date-time":"2020-10-02T12:28:48Z","timestamp":1601641728000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-53733-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319537320","9783319537337"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-53733-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}