{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T19:51:14Z","timestamp":1791057074827,"version":"4.1.0"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,3,6]],"date-time":"2010-03-06T00:00:00Z","timestamp":1267833600000},"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":[[2011,1]]},"DOI":"10.1007\/s10817-010-9167-0","type":"journal-article","created":{"date-parts":[[2010,3,5]],"date-time":"2010-03-05T10:45:51Z","timestamp":1267785951000},"page":"1-42","source":"Crossref","is-referenced-by-count":9,"title":["Resolution with Order and Selection for Hybrid Logics"],"prefix":"10.1007","volume":"46","author":[{"given":"Carlos","family":"Areces","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Gor\u00edn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2010,3,6]]},"reference":[{"key":"9167_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Manna, Z.: Modal theorem proving. In: Proceedings of the 8th International Conference on Automated Deduction, pp. 172\u2013189 (1986)","DOI":"10.1007\/3-540-16780-3_89"},{"key":"9167_CR2","unstructured":"Abadi, M., Manna, Z.: A timely resolution. In: Proceedings of the 1st IEEE Symposium on Logic in Computer Science, pp. 176\u2013186 (1986)"},{"issue":"1\u20132","key":"9167_CR3","first-page":"155","volume":"55","author":"R Achmidt","year":"2009","unstructured":"Achmidt, R.: A new methodology for developing deduction methods. Ann. Math. Artif. Intell. 55(1\u20132), 155\u2013187 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9167_CR4","unstructured":"Areces, C.: Logic engineering. The case of description and hybrid logics. Ph.D. thesis, Institute for Logic, Language and Computation, University of Amsterdam (2000)"},{"key":"9167_CR5","doi-asserted-by":"crossref","unstructured":"Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Proceedings of the 8th Annual Conference of the EACSL, pp. 307\u2013321 (1999)","DOI":"10.1007\/3-540-48168-0_22"},{"issue":"5","key":"9167_CR6","doi-asserted-by":"crossref","first-page":"653","DOI":"10.1093\/jigpal\/8.5.653","volume":"8","author":"C Areces","year":"2000","unstructured":"Areces, C., Blackburn, P., Marx, M.: The computational complexity of hybrid temporal logics. Log. J. IGPL 8(5), 653\u2013679 (2000)","journal-title":"Log. J. IGPL"},{"issue":"5","key":"9167_CR7","doi-asserted-by":"crossref","first-page":"717","DOI":"10.1093\/logcom\/11.5.717","volume":"11","author":"C Areces","year":"2001","unstructured":"Areces, C., de Nivelle, H., de Rijke, M.: Resolution in modal, description and hybrid logic. J. Log. Comput. 11(5), 717\u2013736 (2001)","journal-title":"J. Log. Comput."},{"key":"9167_CR8","unstructured":"Areces, C., Gennari, R., Heguiabehere, J., de Rijke, M.: Tree-based heuristics in modal theorem proving. In: Horn, W. (ed.) Proceedings of ECAI 2000, pp. 199\u2013203 (2000)"},{"key":"9167_CR9","series-title":"LNCS","first-page":"125","volume-title":"Proceedings of LPAR 2004","author":"C Areces","year":"2005","unstructured":"Areces, C., Gor\u00edn, D.: Ordered resolution with selection for $\\mathcal{H}(@)$ . In: Baader, F., Voronkov, A. (eds.) Proceedings of LPAR 2004. LNCS, vol. 3452, pp. 125\u2013141. Springer, New York (2005)"},{"key":"9167_CR10","first-page":"821","volume-title":"Handbook of Modal Logics","author":"C Areces","year":"2006","unstructured":"Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics, pp.\u00a0821\u2013868. Elsevier, Amsterdam (2006)"},{"issue":"1","key":"9167_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00302639","volume":"6","author":"Y Auffray","year":"1990","unstructured":"Auffray, Y., Enjalbert, P., Hebrard, J.: Strategies for modal resolution: results and problems. J. Autom. Reason. 6(1), 1\u201338 (1990)","journal-title":"J. Autom. Reason."},{"key":"9167_CR12","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"9167_CR13","first-page":"353","volume-title":"Automated Deduction\u2014a Basis for Applications, vol. I","author":"L Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Equational reasoning in saturation-based theorem proving. In: Automated Deduction\u2014a Basis for Applications, vol. I, pp. 353\u2013397. Kluwer, Boston (1998)"},{"key":"9167_CR14","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning, vol. 1, chap. 2","author":"L Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, chap. 2, pp. 19\u201399. Elsevier, Amsterdam (2001)"},{"key":"9167_CR15","doi-asserted-by":"crossref","unstructured":"Bieber, P., Fari\u00f1as del Cerro, L., Herzig, A.: MOLOG: a modal PROLOG. In: Proceedings of the 9th International Conference on Automated Deduction, pp. 762\u2013763 (1988)","DOI":"10.1007\/BFb0012886"},{"issue":"3","key":"9167_CR16","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1093\/jigpal\/8.3.339","volume":"8","author":"P Blackburn","year":"2000","unstructured":"Blackburn, P.: Representation, reasoning, and relational structures: a hybrid logic manifesto. Log. J. IGPL 8(3), 339\u2013365 (2000)","journal-title":"Log. J. IGPL"},{"key":"9167_CR17","volume-title":"Modal Logic","author":"P Blackburn","year":"2002","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2002)"},{"key":"9167_CR18","volume-title":"Handbook of Modal Logics","year":"2006","unstructured":"Blackburn, P., Wolter, F., van Benthem, J. (eds.): Handbook of Modal Logics. Elsevier, Amsterdam (2006)"},{"key":"9167_CR19","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1002\/malq.19860323106","volume":"32","author":"M Cialdea","year":"1986","unstructured":"Cialdea, M., Fari\u00f1as del Cerro, L.: A modal Herbrand\u2019s property. Z. Math. Log. Grundl. Math. 32, 523\u2013530 (1986)","journal-title":"Z. Math. Log. Grundl. Math."},{"key":"9167_CR20","volume-title":"Model Checking","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT, Cambridge (2000)"},{"issue":"1","key":"9167_CR21","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S0747-7171(02)00092-5","volume":"35","author":"H Nivelle de","year":"2003","unstructured":"de Nivelle, H., de Rijke, M.: Deciding the guarded fragments by resolution. J. Symb. Comput. 35(1), 21\u201358 (2003)","journal-title":"J. Symb. Comput."},{"issue":"3","key":"9167_CR22","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1093\/jigpal\/8.3.265","volume":"8","author":"H Nivelle de","year":"2000","unstructured":"de Nivelle, H., Schmidt, R., Hustadt, U.: Resolution-based methods for modal logics. Log. J. IGPL 8(3), 265\u2013292 (2000)","journal-title":"Log. J. IGPL"},{"issue":"1","key":"9167_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(89)90137-0","volume":"65","author":"P Enjalbert","year":"1989","unstructured":"Enjalbert, P., Fari\u00f1as del Cerro, L.: Modal resolution in clausal form. Theor. Comp. Sci. 65(1), 1\u201333 (1989)","journal-title":"Theor. Comp. Sci."},{"issue":"2","key":"9167_CR24","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0020-0190(82)90085-0","volume":"14","author":"L Fari\u00f1as del Cerro","year":"1982","unstructured":"Fari\u00f1as del Cerro, L.: A simple deduction method for modal logic. Inf. Process. Lett. 14(2), 47\u201351 (1982)","journal-title":"Inf. Process. Lett."},{"key":"9167_CR25","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-3-642-82453-1_2","volume-title":"Logics and Models of Concurrent Systems","author":"L Fari\u00f1as del Cerro","year":"1985","unstructured":"Fari\u00f1as del Cerro, L.: Resolution modal logic. In: Apt, K. (ed.) Logics and Models of Concurrent Systems, pp. 27\u201355. Springer, Berlin (1985)"},{"issue":"1","key":"9167_CR26","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/BF03037381","volume":"4","author":"L Fari\u00f1as del Cerro","year":"1986","unstructured":"Fari\u00f1as del Cerro, L.: MOLOG: a system that extends PROLOG with modal logic. New Gener. Comput. 4(1), 35\u201350 (1986)","journal-title":"New Gener. Comput."},{"issue":"1","key":"9167_CR27","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1093\/logcom\/1.1.83","volume":"1","author":"M Fitting","year":"1990","unstructured":"Fitting, M.: Destructive modal resolution. J. Log. Comput. 1(1), 83\u201397 (1990)","journal-title":"J. Log. Comput."},{"key":"9167_CR28","first-page":"295","volume-title":"LICS \u201999: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science","author":"H Ganzinger","year":"1999","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: LICS \u201999: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p. 295. IEEE Computer Society, Los Alamitos (1999)"},{"key":"9167_CR29","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/3-540-48754-9_17","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods, Intl. Conf. (TABLEAUX\u201999)","author":"M Giese","year":"1999","unstructured":"Giese, M., Ahrendt, W.: Hilbert\u2019s \u03b5-terms in automated theorem proving. In: Murray, N. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods, Intl. Conf. (TABLEAUX\u201999). LNAI, vol.\u00a01617, pp. 171\u2013185. Springer, Berlin (1999)"},{"key":"9167_CR30","doi-asserted-by":"crossref","first-page":"1719","DOI":"10.2307\/2586808","volume":"64","author":"E Gr\u00e4del","year":"1999","unstructured":"Gr\u00e4del, E.: On the restraining power of guards. J. Symb. Log. 64, 1719\u20131742 (1999)","journal-title":"J. Symb. Log."},{"key":"9167_CR31","first-page":"393","volume-title":"Current Trends in Theoretical Computer Science: Entering the 21st Centuary","author":"E Gr\u00e4del","year":"2001","unstructured":"Gr\u00e4del, E.: Why are modal logics so robustly decidable? In: Current Trends in Theoretical Computer Science: Entering the 21st Centuary, pp. 393\u2013408. World Scientific, Singapore (2001)"},{"key":"9167_CR32","unstructured":"Herbrand, J.: Recherches sur la th\u00e9orie de la d\u00e9monstrations. Ph.D. thesis, Sorbone (1930). Reprinted In: Goldfarb, W. (ed.) Logical Writings. Reidel, Dordrecht (1971)"},{"key":"9167_CR33","volume-title":"Grundlagen der Mathematik, vol. 2","author":"D Hilbert","year":"1939","unstructured":"Hilbert, D., Bernays, P.: Grundlagen der Mathematik, vol. 2. Springer, Berlin (1939)"},{"issue":"2","key":"9167_CR34","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1023\/A:1015067300005","volume":"28","author":"U Hustadt","year":"2002","unstructured":"Hustadt, U., Schmidt, R.: Using resolution for testing modal satisfiability and building models. J. Autom. Reason. 28(2), 205\u2013232 (2002)","journal-title":"J. Autom. Reason."},{"key":"9167_CR35","unstructured":"Kazakov, Y.: Saturation-based decision procedures for extensions of the guarded fragment. Ph.D. thesis, Universit\u00e4t des Saarlandes (2006)"},{"issue":"2\u20133","key":"9167_CR36","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/s10817-007-9090-1","volume":"40","author":"Y Kazakov","year":"2008","unstructured":"Kazakov, Y., Motik, B.: A resolution-based decision procedure for SHOIQ. J. Autom. Reason. 40(2\u20133), 89\u2013116 (2008)","journal-title":"J. Autom. Reason."},{"key":"9167_CR37","first-page":"263","volume-title":"Computational Algebra","author":"D Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Algebra, pp. 263\u2013297. Pergamon, Oxford (1970)"},{"key":"9167_CR38","volume-title":"Mathematical Logic and Hilbert\u2019s \u03b5-symbol","author":"A Leisenring","year":"1969","unstructured":"Leisenring, A.: Mathematical Logic and Hilbert\u2019s \u03b5-symbol. MacDonald, London (1969)"},{"key":"9167_CR39","first-page":"1149","volume-title":"Handbook of Modal Logics","author":"S Lindstr\u00f6m","year":"2006","unstructured":"Lindstr\u00f6m, S., Segerberg, K.: Modal logic and philosophy. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics, pp. 1149\u20131214. Elsevier, Amsterdam (2006)"},{"key":"9167_CR40","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1090\/trans2\/143\/01","volume":"143","author":"G Mints","year":"1989","unstructured":"Mints, G.: Resolution calculi for modal logics. Am. Math. Soc. Transl. 143, 1\u201314 (1989)","journal-title":"Am. Math. Soc. Transl."},{"key":"9167_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/3-540-52335-9_55","volume-title":"Proceedings of COLOG-88, Tallin","author":"G Mints","year":"1990","unstructured":"Mints, G.: Gentzen-type systems and resolution rules, part 1: propositional logic. In: Proceedings of COLOG-88, Tallin. Lecture Notes in Computer Science, vol. 417, pp. 198\u2013231. Springer, Berlin (1990)"},{"key":"9167_CR42","doi-asserted-by":"crossref","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 62, 117\u2013134 (2007)","journal-title":"J. Algorithms"},{"key":"9167_CR43","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning, vol. 1, chap. 7","author":"R Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, chap. 7, pp. 371\u2013443. Elsevier, Amsterdam (2001)"},{"key":"9167_CR44","unstructured":"Ohlbach, H.: A resolution calculus for modal logics. Ph.D. thesis, Universit\u00e4t Kaiserslautern (1988)"},{"key":"9167_CR45","first-page":"376","volume-title":"IJCAR \u201901: Proceedings of the First International Joint Conference on Automated Reasoning","author":"A Riazanov","year":"2001","unstructured":"Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: IJCAR \u201901: Proceedings of the First International Joint Conference on Automated Reasoning, pp. 376\u2013380. Springer, Berlin (2001)"},{"key":"9167_CR46","volume-title":"Handbook of Automated Reasoning","year":"2001","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)"},{"issue":"1","key":"9167_CR47","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J Robinson","year":"1965","unstructured":"Robinson, J.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"9167_CR48","first-page":"189","volume-title":"Advances in Modal Logic, vol. 1","author":"R Schmidt","year":"1998","unstructured":"Schmidt, R.: Resolution is a decision procedure for many propositional modal logics. In: Advances in Modal Logic, vol. 1, pp. 189\u2013208. CSLI, Stanford (1998)"},{"issue":"4","key":"9167_CR49","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1023\/A:1006043519663","volume":"22","author":"R Schmidt","year":"1999","unstructured":"Schmidt, R.: Decidability by resolution for propositional modal logics. J. Autom. Reason. 22(4), 379\u2013396 (1999)","journal-title":"J. Autom. Reason."},{"key":"9167_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/978-3-540-24615-2_3","volume-title":"Theory and Applications of Relational Structures and Knowledge Instruments","author":"R Schmidt","year":"2003","unstructured":"Schmidt, R., Hustadt, U.: Mechanised reasoning and model generation for extended modal logics. In: de Swart, H., Orlowska, E., Schmidt, G., Roubens, M. (eds.) Theory and Applications of Relational Structures and Knowledge Instruments. Lecture Notes in Computer Science, vol. 2929, pp. 38\u201367. Springer, Berlin (2003)"},{"key":"9167_CR51","first-page":"149","volume-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 31","author":"M Vardi","year":"1997","unstructured":"Vardi, M.: Why is modal logic so robustly decidable? In: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 31, pp. 149\u2013184. AMS, Providence (1997)","edition":"31"},{"key":"9167_CR52","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: Algorithms, datastructures, and other issues in efficient automated deduction. In: Proceedings of IJCAR 2001. LNAI, vol. 2083, pp. 13\u201328 (2001)","DOI":"10.1007\/3-540-45744-5_3"},{"key":"9167_CR53","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/3-540-48660-7_34","volume-title":"CADE-16: Proceedings of the 16th International Conference on Automated Deduction","author":"C Weidenbach","year":"1999","unstructured":"Weidenbach, C.: System description: SPASS version 1.0.0. In: CADE-16: Proceedings of the 16th International Conference on Automated Deduction, pp. 378\u2013382. Springer, Berlin (1999)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9167-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9167-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9167-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:50Z","timestamp":1559265710000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9167-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3,6]]},"references-count":53,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["9167"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9167-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,3,6]]}}}