{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:07:55Z","timestamp":1725829675643},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243115"},{"type":"electronic","value":"9783319243122"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24312-2_4","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T14:06:46Z","timestamp":1441894006000},"page":"38-53","source":"Crossref","is-referenced-by-count":6,"title":["Modal Tableau Systems with Blocking and Congruence Closure"],"prefix":"10.1007","author":[{"given":"Renate A.","family":"Schmidt","sequence":"first","affiliation":[]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"4_CR2","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. Studia Logica\u00a069, 5\u201340 (2001)","journal-title":"Studia Logica"},{"issue":"2","key":"4_CR3","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1023\/B:JARS.0000009518.26415.49","volume":"31","author":"L. Bachmair","year":"2003","unstructured":"Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. Journal of Automated Reasoning\u00a031(2), 129\u2013168 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/11814771_11","volume-title":"Automated Reasoning","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-up model generation methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 125\u2013139. Springer, Heidelberg (2006)"},{"issue":"1","key":"4_CR5","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1093\/logcom\/7.1.39","volume":"7","author":"B. Beckert","year":"1997","unstructured":"Beckert, B.: Semantic tableaux with equality. Journal of Logic and Computation\u00a07(1), 39\u201358 (1997)","journal-title":"Journal of Logic and Computation"},{"issue":"3","key":"4_CR6","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1093\/logcom\/exm014","volume":"17","author":"T. Bolander","year":"2007","unstructured":"Bolander, T., Blackburn, P.: Termination for hybrid tableaus. Journal of Logic and Computation\u00a017(3), 517\u2013554 (2007)","journal-title":"Journal of Logic and Computation"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1007\/3-540-50241-6_28","volume-title":"CSL \u201987","author":"F. Bry","year":"1988","unstructured":"Bry, F., Manthey, R.: Proving finite satisfiability of deductive databases. In: B\u00f6rger, E., Kleine B\u00fcning, H., Richter, M.M. (eds.) CSL 1987. LNCS, vol.\u00a0329, pp. 44\u201355. Springer, Heidelberg (1988)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 611\u2013706. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50012-6"},{"issue":"1-3","key":"4_CR9","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/s10817-006-9050-1","volume":"38","author":"M. Giese","year":"2007","unstructured":"Giese, M.: Superposition-based equality handling for analytic tableaux. Journal of Automated Reasoning\u00a038(1-3), 127\u2013153 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Gor\u00e9, R.: Tableau methods for modal and temporal logics. In: D\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 297\u2013396. Kluwer (1999)","DOI":"10.1007\/978-94-017-1754-0_6"},{"key":"4_CR11","unstructured":"Kaminski, M.: Incremental Decision Procedures for Modal Logics with Nominals and Eventualities. PhD thesis, Universit\u00e4t des Saarlandes, Germany (2012)"},{"key":"4_CR12","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/j.entcs.2009.02.039","volume":"231","author":"M. Kaminski","year":"2009","unstructured":"Kaminski, M., Smolka, G.: Hybrid tableaux for the difference modality. Electronic Notes in Theoretical Computer Science\u00a0231, 241\u2013257 (2009)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"3","key":"4_CR13","first-page":"99","volume":"4","author":"T. K\u00e4ufl","year":"1990","unstructured":"K\u00e4ufl, T., Zabel, N.: Cooperation of decision procedures in a tableau-based theorem prover. Revue d\u2019Intelligence Artificielle\u00a04(3), 99\u2013126 (1990)","journal-title":"Revue d\u2019Intelligence Artificielle"},{"key":"4_CR14","unstructured":"Khodadadi, M.: Exploration of Variations of Unrestricted Blocking for Description Logics. PhD thesis, The University of Manchester, UK (2015)"},{"key":"4_CR15","unstructured":"Khodadadi, M., Schmidt, R.A., Tishkovsky, D.: An abstract tableau calculus for the description logic ${\\mathcal SHOI}$ using unrestricted blocking and rewriting. In: Proc. DL 2012. CEUR Workshop Proc., vol. 846. CEUR-WS.org (2012)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-642-40537-2_17","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M. Khodadadi","year":"2013","unstructured":"Khodadadi, M., Schmidt, R.A., Tishkovsky, D.: A refined tableau calculus with controlled blocking for the description logic $\\mathcal{SHOI}$ . In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol.\u00a08123, pp. 188\u2013202. Springer, Heidelberg (2013)"},{"issue":"2","key":"4_CR17","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the ACM"},{"issue":"4","key":"4_CR18","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. Information and Computation\u00a0205(4), 557\u2013580 (2007)","journal-title":"Information and Computation"},{"issue":"6","key":"4_CR19","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/978-3-540-76298-0_32","volume-title":"The Semantic Web","author":"R.A. Schmidt","year":"2007","unstructured":"Schmidt, R.A., Tishkovsky, D.: Using tableau to decide expressive description logics with role negation. In: Aberer, K., et al. (eds.) ASWC 2007 and ISWC 2007. LNCS, vol.\u00a04825, pp. 438\u2013451. Springer, Heidelberg (2007)"},{"issue":"2","key":"4_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-7(2:6)2011","volume":"7","author":"R.A. Schmidt","year":"2011","unstructured":"Schmidt, R.A., Tishkovsky, D.: Automated synthesis of tableau calculi. Logical Methods in Computer Science\u00a07(2), 1\u201332 (2011)","journal-title":"Logical Methods in Computer Science"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Schmidt, R.A., Tishkovsky, D.: Using tableau to decide description logics with full role negation and identity. ACM Transactions on Computational Logic\u00a015(1) (2014)","DOI":"10.1145\/2559947"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Schmidt, R.A., Waldmann, U.: Modal tableau systems with blocking and congruence closure. eScholar Report uk-ac-man-scw:268816, University of Manchester (2015)","DOI":"10.1007\/978-3-319-24312-2_4"},{"key":"4_CR24","unstructured":"Tishkovsky, D., Schmidt, R.A.: Refinement in the tableau synthesis framework (2013). arXiv e-Print 1305.3131v1 [cs.LO]"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"492","DOI":"10.1007\/978-3-642-33353-8_41","volume-title":"Logics in Artificial Intelligence","author":"D. Tishkovsky","year":"2012","unstructured":"Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: The tableau prover generator MetTeL2. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS, vol.\u00a07519, pp. 492\u2013495. Springer, Heidelberg (2012)"}],"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-319-24312-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,30]],"date-time":"2019-08-30T09:47:36Z","timestamp":1567158456000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24312-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243115","9783319243122"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24312-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}