{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:18:28Z","timestamp":1725491908424},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730989"},{"type":"electronic","value":"9783540730996"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73099-6_4","type":"book-chapter","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T07:04:02Z","timestamp":1189753442000},"page":"11-27","source":"Crossref","is-referenced-by-count":16,"title":["Axiom Pinpointing in General Tableaux"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[]},{"given":"Rafael","family":"Pe\u00f1aloza","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","first-page":"364","volume-title":"Proc. of IJCAI\u00a02005","author":"F. Baader","year":"2005","unstructured":"Baader, F., Brandt, S., Lutz, C.: Pushing the $\\mathcal{EL}$ envelope. In: Proc. of IJCAI\u00a02005, pp. 364\u2013369. Morgan Kaufmann, Los Alamitos (2005)"},{"key":"4_CR2","volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","author":"F. Baader","year":"2003","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F.: The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)"},{"key":"4_CR3","unstructured":"Baader, F., Hanschke, P.: A scheme for integrating concrete domains into concept languages. Technical Report RR-91-10, Deutsches Forschungszentrum f\u00fcr K\u00fcnstliche Intelligenz (DFKI) (1991)"},{"issue":"2-4","key":"4_CR4","first-page":"247","volume":"57","author":"F. Baader","year":"2003","unstructured":"Baader, F., Hladik, J., Lutz, C., Wolter, F.: From tableaux to automata for description logics. Fundamenta Informaticae\u00a057(2-4), 247\u2013279 (2003)","journal-title":"Fundamenta Informaticae"},{"key":"4_CR5","doi-asserted-by":"publisher","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. of Automated Reasoning\u00a014, 149\u2013180 (1995)","journal-title":"J. of Automated Reasoning"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Baader, F., Pe\u00f1aloza, R.: Axiom pinpointing in general tableaux. LTCS-Report 07-01, TU Dresden, Germany (2007), http:\/\/lat.inf.tu-dresden.de\/research\/reports.html","DOI":"10.25368\/2022.159"},{"key":"4_CR7","doi-asserted-by":"publisher","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. Studia Logica\u00a069, 5\u201340 (2001)","journal-title":"Studia Logica"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","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.) Practical Aspects of Declarative Languages. LNCS, vol.\u00a03350, Springer, Heidelberg (2005)"},{"issue":"3-4","key":"4_CR9","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1023\/A:1018924526592","volume":"23","author":"G. Davydov","year":"1998","unstructured":"Davydov, G., Davydova, I., B\u00fcning, H.K.: An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF. Ann.of Mathematics and Artificial Intelligence\u00a023(3-4), 229\u2013245 (1998)","journal-title":"Ann.of Mathematics and Artificial Intelligence"},{"key":"4_CR10","volume-title":"Computers and Intractability \u2014 A guide to NP-completeness","author":"M.R. Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability \u2014 A guide to NP-completeness. W.H. Freeman and Company, San Francisco (CA, USA) (1979)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Haarslev, V., M\u00f6ller, R.: RACER system description. In Proc. of IJCAR\u00a02001 (2001)","DOI":"10.1007\/3-540-45744-5_59"},{"key":"4_CR12","first-page":"38","volume-title":"Proc. of German Workshop on AI","author":"B. Hollunder","year":"1990","unstructured":"Hollunder, B.: Hybrid inferences in KL-ONE-based knowledge representation systems. In: Proc. of German Workshop on AI, pp. 38\u201347. Springer, Heidelberg (1990)"},{"key":"4_CR13","unstructured":"Horrocks, I.: Using an expressive description logic: FaCT or fiction. In: Proc. of KR 1998, pp. 636\u2013647 (1998)"},{"issue":"1","key":"4_CR14","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. J. of Web Semantics\u00a01(1), 7\u201326 (2003)","journal-title":"J. of Web Semantics"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Kalyanpur, A., Parsia, B., Sirin, E., Cuenca-Grau, B., Hendler, J.: Swoop: A Web ontology editing browser. J. of Web Semantics 4(2) (2005)","DOI":"10.1016\/j.websem.2005.10.001"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Knublauch, H., Fergerson, R.W., Noy, N.F., Musen, M.A.: The Prot\u00e9g\u00e9 OWL plugin: An open development environment for semantic web applications. In: Proceedings of the Third Int. Semantic Web Conf, Hiroshima, Japan (2004)","DOI":"10.1007\/978-3-540-30475-3_17"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"M.H. Liffiton","year":"2005","unstructured":"Liffiton, M.H., Sakallah, K.A.: On finding all minimally unsatisfiable subformulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, Springer, Heidelberg (2005)"},{"key":"4_CR18","unstructured":"Meyer, T., Lee, K., Booth, R., Pan, J.Z.: Finding maximally satisfiable terminologies for the description logic $\\mathcal{{ALC}}$ . In: Proc. of AAAI\u00a02006, AAAI Press\/The MIT Press, Cambridge (2006)"},{"key":"4_CR19","first-page":"311","volume-title":"Handbook on Ontologies, International Handbooks on Information Systems","author":"D. Oberle","year":"2004","unstructured":"Oberle, D., Volz, R., Motik, B., Staab, S.: An extensible ontology software environment. In: Handbook on Ontologies, International Handbooks on Information Systems, pp. 311\u2013333. Springer, Heidelberg (2004)"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/1060745.1060837","volume-title":"Proc. of WWW 2005","author":"B. Parsia","year":"2005","unstructured":"Parsia, B., Sirin, E., Kalyanpur, A.: Debugging OWL ontologies. In: Proc. of WWW 2005, pp. 633\u2013640. ACM, New York (2005)"},{"issue":"1","key":"4_CR21","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. Artificial Intelligence\u00a032(1), 57\u201395 (1987)","journal-title":"Artificial Intelligence"},{"key":"4_CR22","unstructured":"Schlobach, S.: Diagnosing terminologies. In: Proc. of AAAI 2005, pp. 670-675. AAAI Press\/The MIT Press, Cambridge (2005)"},{"key":"4_CR23","first-page":"355","volume-title":"Proc. of IJCAI\u00a02003","author":"S. Schlobach","year":"2003","unstructured":"Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: Proc. of IJCAI\u00a02003, Acapulco, Mexico, pp. 355\u2013362. Morgan Kaufmann, San Francisco, Los Alamitos (2003)"},{"issue":"1","key":"4_CR24","doi-asserted-by":"publisher","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. Artificial Intelligence\u00a048(1), 1\u201326 (1991)","journal-title":"Artificial Intelligence"},{"key":"4_CR25","unstructured":"Sirin, E., Parsia, B.: Pellet: An OWL DL reasoner. In: Proc. of DL 2004, pp. 212\u2013213 (2004)"},{"key":"4_CR26","unstructured":"Spackman, K.A., Campbell, K.E., Cote, R.A.: SNOMED RT: A reference terminology for health care. J. of the American Medical Informatics Association, Fall Symposium Supplement, pp. 640\u2013644 (1997)"},{"key":"4_CR27","first-page":"10880","volume-title":"Proc. of DATE 2003","author":"L. Zhang","year":"2003","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Proc. of DATE 2003, pp. 10880\u201310885. IEEE Computer Society Press, Washington (2003)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73099-6_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T04:14:07Z","timestamp":1684037647000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73099-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730989","9783540730996"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73099-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}