{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T15:10:03Z","timestamp":1748617803850,"version":"3.41.0"},"publisher-location":"Cham","reference-count":26,"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_13","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T14:06:46Z","timestamp":1441894006000},"page":"185-200","source":"Crossref","is-referenced-by-count":7,"title":["A Modal-Layered Resolution Calculus for K"],"prefix":"10.1007","author":[{"given":"Cl\u00e1udia","family":"Nalon","sequence":"first","affiliation":[]},{"given":"Ullrich","family":"Hustadt","sequence":"additional","affiliation":[]},{"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-48660-7_13","volume-title":"Automated Deduction - CADE-16","author":"C. Areces","year":"1999","unstructured":"Areces, C., de Nivelle, H., de Rijke, M.: Prefixed resolution: A resolution method for modal and description logics. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 187\u2013201. Springer, Heidelberg (1999)"},{"key":"13_CR2","unstructured":"Areces, C., Gennari, R., Heguiabehere, J., Rijke, M.D.: Tree-based heuristics in modal theorem proving. In: Proc. of ECAI 2000. IOS Press (2000)"},{"issue":"1","key":"13_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-010-9167-0","volume":"46","author":"C. Areces","year":"2011","unstructured":"Areces, C., Gor\u00edn, D.: Resolution with order and selection for hybrid logics. Journal of Automated Reasoning\u00a046(1), 1\u201342 (2011)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR4","unstructured":"Areces, C., Heguiabehere, J.: HyLoRes: A hybrid logic prover, September 18 2002, http:\/\/citeseer.ist.psu.edu\/619572.html ; http:\/\/turing.wins.uva.nl\/~carlos\/Papers\/aiml2002-2.ps.gz"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/3-540-52885-7_105","volume-title":"10th International Conference on Automated Deduction","author":"L. Bachmair","year":"1990","unstructured":"Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 427\u2013441. Springer, Heidelberg (1990)"},{"key":"13_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"P. Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)"},{"issue":"1","key":"13_CR7","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1093\/logcom\/2.1.5","volume":"2","author":"V. Goranko","year":"1992","unstructured":"Goranko, V., Passy, S.: Using the universal modality: gains and questions. Journal of Logic and Computation\u00a02(1), 5\u201330 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R.: Automated Deduction in Multiple-Valued Logics. Oxford University Press (1993)","DOI":"10.1093\/oso\/9780198539896.001.0001"},{"issue":"3","key":"13_CR9","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"J.Y. Halpern","year":"1992","unstructured":"Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence\u00a054(3), 319\u2013379 (1992)","journal-title":"Artificial Intelligence"},{"key":"13_CR10","first-page":"87","volume-title":"Machine Intelligence","author":"P.J. Hayes","year":"1969","unstructured":"Hayes, P.J., Kowalski, R.A.: Semantic trees in automatic theorem proving. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol.\u00a05, pp. 87\u2013101. Elsevier, New York (1969)"},{"key":"13_CR11","first-page":"181","volume-title":"Handbook of Modal Logic","author":"I.R. Horrocks","year":"2006","unstructured":"Horrocks, I.R., Hustadt, U., Sattler, U., Schmidt, R.: Computational modal logic. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, pp. 181\u2013245. Elsevier Science Inc., New York (2006)"},{"key":"13_CR12","unstructured":"Hustadt, U., Konev, B.: TRP++: A temporal resolution prover. In: Baaz, M., Makowsky, J., Voronkov, A. (eds.) Collegium Logicum, pp. 65\u201379. Kurt G\u00f6del Society (2004)"},{"key":"13_CR13","unstructured":"Lee, R.C.T.: A completeness theorem and computer proram for finding theorems derivable from given axioms. Ph.D. thesis, Berkeley (1967)"},{"key":"13_CR14","series-title":"Texts in Theoretical Computer Science an EATCS Series","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-68804-8_7","volume-title":"Finite Model Theory and Its Applications","author":"M. Marx","year":"2007","unstructured":"Marx, M., Venema, Y.: Local variations on a loose theme: Modal logic and decidability. In: Finite Model Theory and Its Applications. Texts in Theoretical Computer Science an EATCS Series, pp. 371\u2013429. Springer, Heidelberg (2007)"},{"issue":"1\u20133","key":"13_CR15","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/0004-3702(72)90047-1","volume":"3","author":"E. Minicozzi","year":"1972","unstructured":"Minicozzi, E., Reiter, R.: A note on linear resolution strategies in consequence-finding. Artificial Intelligence\u00a03(1\u20133), 175\u2013180 (1972)","journal-title":"Artificial Intelligence"},{"key":"13_CR16","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.jalgor.2007.04.001","volume":"62","author":"C. Nalon","year":"2007","unstructured":"Nalon, C., Dixon, C.: Clausal resolution for normal modal logics. J. Algorithms\u00a062, 117\u2013134 (2007), http:\/\/dl.acm.org\/citation.cfm?id=1316091.1316347","journal-title":"J. Algorithms"},{"issue":"4","key":"13_CR17","doi-asserted-by":"crossref","first-page":"351","DOI":"10.3233\/FUN-2006-70404","volume":"70","author":"L.A. Nguyen","year":"2006","unstructured":"Nguyen, L.A.: Negative ordered hyper-resolution as a proof procedure for disjunctive logic programming. Fundam. Inform\u00a070(4), 351\u2013366 (2006)","journal-title":"Fundam. Inform"},{"key":"13_CR18","first-page":"293","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.A.: A Structure-Preserving Clause Form Translation. Journal of Logic and Computation\u00a02, 293\u2013304 (1986)","journal-title":"Journal of Logic and Computation"},{"key":"13_CR19","first-page":"227","volume":"1","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: Automatic Deduction with Hyper-resolution. International Journal of Computer Mathematics\u00a01, 227\u2013234 (1965)","journal-title":"International Journal of Computer Mathematics"},{"key":"13_CR20","unstructured":"Schild, K.: A Correspondence theory for terminological logics. In: Proceedings of the 12th IJCAI, pp. 466\u2013471. Springer (1991)"},{"key":"13_CR21","unstructured":"Schulz, S.: The E theorem prover (2013), http:\/\/wwwlehre.dhbw-stuttgart.de\/~sschulz\/E\/E.html"},{"key":"13_CR22","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.artint.2014.01.002","volume":"209","author":"F. Simancik","year":"2014","unstructured":"Simancik, F., Motik, B., Horrocks, I.: Consequence-based and fixed-parameter tractable reasoning in description logics. Artif. Intell.\u00a0209, 29\u201377 (2014)","journal-title":"Artif. Intell."},{"key":"13_CR23","unstructured":"Slagle, J.R., Chang, C.L., Lee, R.C.T.: Completeness theorems for semantic resolution in consequence-finding. In: Proceedings of the 1st IJCAI, pp. 281\u2013286. William Kaufmann, May 1969"},{"key":"13_CR24","unstructured":"Spaan, E.: Complexity of Modal Logics. Ph.D. thesis, University of Amsterdam (1993)"},{"key":"13_CR25","unstructured":"The SPASS Team: Automation of logic: Spass (2010), http:\/\/www.spass-prover.org\/"},{"key":"13_CR26","unstructured":"Voronkov, A.: Vampire, http:\/\/www.vprover.org\/index.cgi"}],"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_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T14:54:50Z","timestamp":1748616890000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24312-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243115","9783319243122"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24312-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}