{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,4]],"date-time":"2026-03-04T06:50:25Z","timestamp":1772607025212,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642405365","type":"print"},{"value":"9783642405372","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40537-2_23","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T12:33:51Z","timestamp":1378902831000},"page":"273-287","source":"Crossref","is-referenced-by-count":2,"title":["Intelligent Tableau Algorithm for DL Reasoning"],"prefix":"10.1007","author":[{"given":"Ming","family":"Zuo","sequence":"first","affiliation":[]},{"given":"Volker","family":"Haarslev","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","unstructured":"Areces, C., Bouma, W., de Rijke, M.: Description logics and feature interaction. In: Proceedings of the International Workshop on Description Logics (DL 1999), Link\u00f6ping, Sweden, pp. 28\u201332 (1999)"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook, 2nd edn. Cambridge University Press (2007)","DOI":"10.1017\/CBO9780511711787"},{"key":"23_CR3","unstructured":"Ding, Y., Haarslev, V.: Tableau caching for description Logics with inverse and transitive roles. In: Proceedings of the 2006 International Workshop on Description Logics (DL 2006), pp. 143\u2013149 (2006)"},{"issue":"1","key":"23_CR4","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0004-3702(00)00070-9","volume":"124","author":"F.M. Donini","year":"2000","unstructured":"Donini, F.M., Massacci, F.: EXPTIME tableaux for \n                    \n                      \n                    \n                    $\\cal{ALC}$\n                  . Artificial Intelligence\u00a0124(1), 87\u2013138 (2000)","journal-title":"Artificial Intelligence"},{"key":"23_CR5","unstructured":"Faddoul, J.: Reasoning algebraically with description logics. PhD thesis, Department of Computer Science and Engineering, Concordia University (2011)"},{"key":"23_CR6","unstructured":"Gor\u00e9, R., Nguyen, L.: Exptime tableaux for \n                    \n                      \n                    \n                    ${\\cal ALC}$\n                   using sound global caching. Journal of Automated Reasoning, 1\u201327 (2011)"},{"key":"23_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-71070-7_25","volume-title":"Automated Reasoning","author":"R. Gor\u00e9","year":"2008","unstructured":"Gor\u00e9, R., Postniece, L.: An experimental evaluation of global caching for \n                    \n                      \n                    \n                    $\\cal{ALC}$\n                   (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 299\u2013305. Springer, Heidelberg (2008)"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/10722086_5","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"V. Haarslev","year":"2000","unstructured":"Haarslev, V., M\u00f6ller, R.: Consistency testing: The RACE experience. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol.\u00a01847, pp. 57\u201361. Springer, Heidelberg (2000)"},{"key":"23_CR9","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/3-540-45744-5_59","volume-title":"Automated Reasoning","author":"V. Haarslev","year":"2001","unstructured":"Haarslev, V., M\u00f6ller, R.: Racer system description. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 701\u2013705. Springer, Heidelberg (2001)"},{"key":"23_CR10","unstructured":"Herbrand, J.: Recherches sur la th\u00e9orie de la d\u00e9monstration. PhD thesis, University of Paris (1930)"},{"key":"23_CR11","unstructured":"Hooker, J.: Satlib - benchmark problems. Website (2011), \n                    \n                      http:\/\/www.cs.ubc.ca\/~hoos\/SATLIB\/benchm.html"},{"key":"23_CR12","unstructured":"Horrocks, I.: Using an expressive description logic: FaCT or fiction? In: Proc. of KR 1998, pp. 636\u2013647 (1998)"},{"key":"23_CR13","unstructured":"Horrocks, I., Patel-Schneider, P.: DL systems comparison. In: Proc. of the 1998 Description Logic Workshop (DL 1998). CEUR, vol.\u00a011, pp. 55\u201357 (1998)"},{"key":"23_CR14","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1613\/jair.2811","volume":"36","author":"B. Motik","year":"2009","unstructured":"Motik, B., Shearer, R., Horrocks, I.: Hypertableau reasoning for description logics. Journal of Artificial Intelligence Research\u00a036, 165\u2013228 (2009)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"23_CR15","unstructured":"Ryan, L.O.: Efficient algorithms for clause learning SAT solvers. Master\u2019s thesis, Simon Fraser University, BC, Canada (2004)"},{"issue":"1","key":"23_CR16","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":"23_CR17","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Vescovi, M.: Automated reasoning in modal and description logics via SAT encoding: the case study of K(m)\/ALC-Satisfiability. Journal of Artificial Intelligence Research\u00a035 (2009)","DOI":"10.1613\/jair.2675"},{"key":"23_CR18","unstructured":"Shearer, R., Motik, B., Horrocks, I.: Hermit: A highly efficient OWL reasoner. In: 5th OWL Experiences and Directions Workshop (2008)"},{"issue":"2","key":"23_CR19","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.websem.2007.03.004","volume":"5","author":"E. Sirin","year":"2007","unstructured":"Sirin, E., Parsia, B., Cuenca Grau, B., Kalyanpur, A., Katz, Y.: Pellet: A practical OWL-DL reasoner. Journal of Web Semantics\u00a05(2), 51\u201353 (2007)","journal-title":"Journal of Web Semantics"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-642-31365-3_40","volume-title":"Automated Reasoning","author":"A. Steigmiller","year":"2012","unstructured":"Steigmiller, A., Liebig, T., Glimm, B.: Extended caching, backjumping and merging for expressive description logics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 514\u2013529. Springer, Heidelberg (2012)"},{"key":"23_CR21","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/11814771_26","volume-title":"Automated Reasoning","author":"D. Tsarkov","year":"2006","unstructured":"Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 292\u2013297. Springer, Heidelberg (2006)"},{"key":"23_CR22","unstructured":"Zhang, L.: Searching for truth: techniques for satisfiability of boolean formulas. PhD thesis, Departement of Electrical Engineering, Princeton University (2003)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40537-2_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T05:36:34Z","timestamp":1558071394000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40537-2_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642405365","9783642405372"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40537-2_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}