{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T01:05:47Z","timestamp":1777424747540,"version":"3.51.4"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,7,2]],"date-time":"2010-07-02T00:00:00Z","timestamp":1278028800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2010,8]]},"DOI":"10.1007\/s10817-010-9181-2","type":"journal-article","created":{"date-parts":[[2010,7,1]],"date-time":"2010-07-01T04:30:12Z","timestamp":1277958612000},"page":"91-129","source":"Crossref","is-referenced-by-count":32,"title":["Automata-Based Axiom Pinpointing"],"prefix":"10.1007","volume":"45","author":[{"given":"Franz","family":"Baader","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":[[2010,7,2]]},"reference":[{"key":"9181_CR1","unstructured":"Baader, F.: Augmenting concept languages by transitive closure of roles: an alternative to terminological cycles. In: Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI\u201991) (1991)"},{"key":"9181_CR2","volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","year":"2003","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)"},{"issue":"9\u201310","key":"9181_CR3","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":"9181_CR4","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. Reason. 14, 149\u2013180 (1995)","journal-title":"J. Autom. Reason."},{"key":"9181_CR5","series-title":"Lecture Notes in Artificial Intelligence","first-page":"11","volume-title":"Proc. of the Int. Conf. on Analytic Tableaux and Related Methods (TABLEAUX 2007)","author":"F Baader","year":"2007","unstructured":"Baader, F., Pe\u00f1aloza, R.: Axiom pinpointing in general tableaux. In: Proc. of the Int. Conf. on Analytic Tableaux and Related Methods (TABLEAUX 2007). Lecture Notes in Artificial Intelligence, vol. 4548, pp. 11\u201327. Springer, Heidelberg (2007)"},{"key":"9181_CR6","series-title":"Lecture Notes in Artificial Intelligence","first-page":"226","volume-title":"Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2008)","author":"F Baader","year":"2008","unstructured":"Baader, F., Pe\u00f1aloza, R.: Automata-based axiom pinpointing. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2008). Lecture Notes in Artificial Intelligence, vol. 5195, pp. 226\u2013241. Springer, Heidelberg (2008)"},{"key":"9181_CR7","doi-asserted-by":"crossref","unstructured":"Baader, F., Pe\u00f1aloza, R.: Blocking and pinpointing in forest tableaux. LTCS-Report LTCS-08-02, Chair for Automata Theory. Institute for Theoretical Computer Science, Dresden University of Technology, Germany. http:\/\/lat.inf.tu-dresden.de\/research\/reports.html (2008)","DOI":"10.25368\/2022.165"},{"key":"9181_CR8","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, 5\u201334 (2010)","journal-title":"J. Log. Comput."},{"key":"9181_CR9","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1013882326814","volume":"69","author":"F Baader","year":"2001","unstructured":"Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Stud. Log. 69, 5\u201340 (2001)","journal-title":"Stud. Log."},{"key":"9181_CR10","volume-title":"Proc. of the International Conference on Representing and Sharing Knowledge Using SNOMED (KR-MED\u201908)","author":"F Baader","year":"2008","unstructured":"Baader, F., Suntisrivaraporn, B.: Debugging SNOMED CT using axiom pinpointing in the description logic $\\mathcal{EL}^+$ . In: Proc. of the International Conference on Representing and Sharing Knowledge Using SNOMED (KR-MED\u201908), Phoenix, Arizona (2008)"},{"key":"9181_CR11","series-title":"Lecture Notes in Artificial Intelligence","first-page":"92","volume-title":"Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2001)","author":"F Baader","year":"2001","unstructured":"Baader, F., Tobies, S.: The inverse method implements the automata approach for modal satisfiability. In: Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2001). Lecture Notes in Artificial Intelligence, vol. 2083, pp. 92\u2013106. Springer, Heidelberg (2001)"},{"key":"9181_CR12","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"9181_CR13","first-page":"84","volume-title":"Proc. of the 16th Int. Joint Conf. on Artificial Intelligence (IJCAI\u201999)","author":"D Calvanese","year":"1999","unstructured":"Calvanese, D., De Giacomo, G., Lenzerini, M.: Reasoning in expressive description logics with fixpoints based on automata on infinite trees. In: Proc. of the 16th Int. Joint Conf. on Artificial Intelligence (IJCAI\u201999), pp. 84\u201389. Morgan Kaufmann, San Mateo (1999)"},{"key":"9181_CR14","unstructured":"Calvanese, D., De Giacomo, G., Lenzerini, M.: 2ATAs make DLs easy. In: Proc. of the 2002 Description Logic Workshop (DL 2002). CEUR Electronic Workshop Proceedings, pp. 107\u2013118. http:\/\/ceur-ws.org\/Vol-53\/ (2002)"},{"issue":"3, 4","key":"9181_CR15","doi-asserted-by":"crossref","first-page":"305","DOI":"10.3233\/FUN-2008-843-402","volume":"84","author":"M Droste","year":"2008","unstructured":"Droste, M., Kuich, W., Rahonis, G.: Multi-valued MSO logics over words and trees. Fundam. Inform. 84(3, 4), 305\u2013327 (2008)","journal-title":"Fundam. Inform."},{"key":"9181_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/11779148_6","volume-title":"Developments in Language Theory","author":"M Droste","year":"2006","unstructured":"Droste, M., Rahonis, G.: Weighted automata and weighted logics on infinite words. In: Ibarra, O.H., Dang, Z. (eds.) Developments in Language Theory. Lecture Notes in Computer Science, vol. 4036, pp. 49\u201358. Springer, Heidelberg (2006)"},{"key":"9181_CR17","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proc. of the 7th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages (POPL\u201980), pp. 163\u2013173 (1980)","DOI":"10.1145\/567446.567462"},{"key":"9181_CR18","volume-title":"General Lattice Theory","author":"G Gr\u00e4tzer","year":"1998","unstructured":"Gr\u00e4tzer, G.: General Lattice Theory, 2nd edn. Birkh\u00e4user, Cambridge (1998)","edition":"2"},{"key":"9181_CR19","series-title":"Lecture Notes in Artificial Intelligence","first-page":"701","volume-title":"Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2001)","author":"V Haarslev","year":"2001","unstructured":"Haarslev, V., M\u00f6ller, R.: RACER system description. In: Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2001). Lecture Notes in Artificial Intelligence, vol. 2083, pp. 701\u2013705. Springer, Heidelberg (2001)"},{"key":"9181_CR20","unstructured":"Horrocks, I.: Using an expressive description logic: FaCT or fiction? In: Proc. of the 6th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR\u201998), pp. 636\u2013647 (1998)"},{"issue":"1","key":"9181_CR21","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/j.websem.2003.07.001","volume":"1","author":"I Horrocks","year":"2003","unstructured":"Horrocks, I., Patel-Schneider, P.F., van Harmelen, F.: From SHIQ and RDF to OWL: the making of a web ontology language. JWS 1(1), 7\u201326 (2003)","journal-title":"JWS"},{"key":"9181_CR22","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":"Proc. of the 6th International Semantic Web Conference and 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea","author":"A Kalyanpur","year":"2007","unstructured":"Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of OWL DL entailments. In: Proc. of the 6th International Semantic Web Conference and 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea. Lecture Notes in Computer Science, vol. 4825, pp. 267\u2013280. Springer, Heidelberg (2007)"},{"key":"9181_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-540-69738-1_14","volume-title":"8th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201907)","author":"O Kupferman","year":"2007","unstructured":"Kupferman, O., Lustig, Y.: Lattice automata. In: Cook, B., Podelski, A., (eds.) 8th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201907). Lecture Notes in Computer Science, vol. 4349, pp. 199\u2013213. Springer, Heidelberg (2007)"},{"key":"9181_CR24","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Safraless decision procedures. In: Proc. of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS05), pp. 531\u2013542. IEEE Computer Society (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"9181_CR25","unstructured":"Lee, K., Meyer, T., Pan, J.Z.: Computing maximally satisfiable terminologies for the description logic $\\mathcal{ALC}$ with GCIs. In: Proc. of the 2006 Description Logic Workshop (DL 2006). CEUR Electronic Workshop Proceedings, vol. 189 (2006)"},{"key":"9181_CR26","first-page":"329","volume-title":"Advances in Modal Logic, vol. 3","author":"C Lutz","year":"2001","unstructured":"Lutz, C., Sattler, U.: The complexity of reasoning with Boolean modal logic. In: Wolter, F., Wansing, H., de Rijke, M., Zakharyaschev, M. (eds.) Advances in Modal Logic, vol. 3, pp. 329\u2013348. CSLI, Stanford (2001)"},{"key":"9181_CR27","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/1060745.1060837","volume-title":"Proc. of the 14th International Conference on World Wide Web (WWW\u201905)","author":"B Parsia","year":"2005","unstructured":"Parsia, B., Sirin, E., Kalyanpur, A.: Debugging OWL ontologies. In: Ellis, A., Hagino, T. (eds.) Proc. of the 14th International Conference on World Wide Web (WWW\u201905), pp. 633\u2013640. ACM, New York (2005)"},{"key":"9181_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. of the 18th Annual Symp. on the Foundations of Computer Science (FOCS\u201977), pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"9181_CR29","first-page":"319","volume-title":"Proc. of the 16th Annual ACM Symp. on Principles of Programming Languages (POPL\u201989)","author":"A Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. of the 16th Annual ACM Symp. on Principles of Programming Languages (POPL\u201989), pp. 319\u2013327. ACM, New York (1989)"},{"key":"9181_CR30","first-page":"1","volume-title":"Proc. of Symp. on Mathematical Logic and Foundations of Set Theory","author":"MO Rabin","year":"1970","unstructured":"Rabin, M.O.: Weakly definable relations and special automata. In: Bar-Hillel, Y. (ed.) Proc. of Symp. on Mathematical Logic and Foundations of Set Theory, pp. 1\u201323. North-Holland Publ., Amsterdam (1970)"},{"issue":"4","key":"9181_CR31","first-page":"455","volume":"12","author":"G Rahonis","year":"2007","unstructured":"Rahonis, G.: Weighted Muller tree automata and weighted logics. J. Autom. Lang. Comb. 12(4), 455\u2013483 (2007)","journal-title":"J. Autom. Lang. Comb."},{"issue":"1","key":"9181_CR32","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."},{"key":"9181_CR33","first-page":"670","volume-title":"Proc. of the 20th Nat. Conf. on Artificial Intelligence (AAAI 2005)","author":"S Schlobach","year":"2005","unstructured":"Schlobach, S.: Diagnosing terminologies. In: Veloso, M.M., Kambhampati, S. (eds.) Proc. of the 20th Nat. Conf. on Artificial Intelligence (AAAI 2005), pp. 670\u2013675. AAAI Press\/The MIT Press, Menlo Park (2005)"},{"key":"9181_CR34","first-page":"355","volume-title":"Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003), Acapulco, Mexico","author":"S Schlobach","year":"2003","unstructured":"Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: Gottlob, G., Walsh, T. (eds.) Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003), Acapulco, Mexico, pp. 355\u2013362. Morgan Kaufmann, Los Altos (2003)"},{"issue":"3","key":"9181_CR35","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., Harmelen, F.: Debugging incoherent terminologies. J. Autom. Reason. 39(3), 317\u2013349 (2007)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9181_CR36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M Schmidt-Schau\u00df","year":"1991","unstructured":"Schmidt-Schau\u00df, M., Smolka, G.: Attributive concept descriptions with complements. Artif. Intell. 48(1), 1\u201326 (1991)","journal-title":"Artif. Intell."},{"issue":"1","key":"9181_CR37","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0304-3975(94)90271-2","volume":"126","author":"H Seidl","year":"1994","unstructured":"Seidl, H.: Finite tree automata with cost functions. Theor. Comput. Sci. 126(1), 113\u2013142 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"9181_CR38","unstructured":"Sirin, E., Parsia, B.: Pellet: an OWL DL reasoner. In: Proc. of the 2004 Description Logic Workshop (DL 2004), pp. 212\u2013213 (2004)"},{"key":"9181_CR39","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5, 285\u2013309 (1955)","journal-title":"Pac. J. Math."},{"key":"9181_CR40","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. In: Proc. of the 16th ACM SIGACT Symp. on Theory of Computing (STOC\u201984), pp. 446\u2013455 (1984)","DOI":"10.1145\/800057.808711"},{"key":"9181_CR41","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"MY Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. A preliminary version appeared in Proc. of the 16th ACM SIGACT symp. on theory of computing (STOC\u201984). J. Comput. Syst. Sci. 32, 183\u2013221 (1986)","journal-title":"J. Comput. Syst. Sci."},{"key":"9181_CR42","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1109\/SFCS.1983.51","volume-title":"Proc. of the 24th Annual Symposium of Foundations of Computer Science (SFCS\u201983)","author":"P Wolper","year":"1983","unstructured":"Wolper, P., Vardi, M.Y., Prasad Sistla, A.: Reasoning about infinite computation paths. In: Proc. of the 24th Annual Symposium of Foundations of Computer Science (SFCS\u201983), pp. 185\u2013194. IEEE Computer Society, Washington (1983)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9181-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9181-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9181-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T12:35:39Z","timestamp":1740227739000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9181-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7,2]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,8]]}},"alternative-id":["9181"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9181-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,7,2]]}}}