{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T22:11:41Z","timestamp":1789942301703,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540252368","type":"print"},{"value":"9783540322757","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32275-7_9","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T21:14:41Z","timestamp":1292879681000},"page":"125-141","source":"Crossref","is-referenced-by-count":3,"title":["Ordered Resolution with Selection for $\\mathcal{H}(@)$"],"prefix":"10.1007","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","reference":[{"key":"9_CR1","unstructured":"Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobald, C., Topi\u0107, D., Weidenbach, C.: System description: SPASS Version 1.0.0. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 187\u2013201. Springer, Heidelberg (1999)"},{"key":"9_CR2","unstructured":"Areces, C.: Logic Engineering. The Case of Description and Hybrid Logics. PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, The Netherlands (October 2000) H(@)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Proc. of the 8th Annual Conference of the EACSL, pp. 307\u2013321 (1999)","DOI":"10.1007\/3-540-48168-0_22"},{"issue":"3","key":"9_CR4","doi-asserted-by":"publisher","first-page":"977","DOI":"10.2307\/2695090","volume":"66","author":"C. Areces","year":"2001","unstructured":"Areces, C., Blackburn, P., Marx, M.: Hybrid logics: Characterization, interpolation and complexity. Journal of Symbolic Logic\u00a066(3), 977\u20131010 (2001)","journal-title":"Journal of Symbolic Logic"},{"issue":"5","key":"9_CR5","doi-asserted-by":"publisher","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. Journal of Logic and Computation\u00a011(5), 717\u2013736 (2001)","journal-title":"Journal of Logic and Computation"},{"key":"9_CR6","unstructured":"Areces, C., Heguiabehere, J.: HyLoRes: A hybrid logic prover based on direct resolution. In: Advances in Modal Logic, Toulouse, France (2002)"},{"key":"9_CR7","unstructured":"Areces, C., Heguiabehere, J.: hGen: A random CNF formula generator for Hybrid Languages. In: Proc. of Methods for Modalities, Nancy, France, vol.\u00a03 (2003)"},{"key":"9_CR8","volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","year":"2003","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)"},{"key":"9_CR9","first-page":"353","volume-title":"Automated deduction\u2014a basis for applications","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.\u00a0I, pp. 353\u2013397. Kluwer, Dordrecht (1998)"},{"key":"9_CR10","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, ch. 2, pp. 19\u201399. Elsevier, Amsterdam (2001)"},{"issue":"3","key":"9_CR11","doi-asserted-by":"publisher","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. Logic Journal of the IGPL\u00a08(3), 339\u2013365 (2000)","journal-title":"Logic Journal of the IGPL"},{"key":"9_CR12","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":"9_CR13","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Volume B: Formal Models and Sematics, vol.\u00a0(B), pp. 243\u2013320. Elsevier and MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"9_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-45653-8_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L. Georgieva","year":"2001","unstructured":"Georgieva, L., Hustadt, U., Schmidt, R.: Computational space efficiency and minimal model generation for guarded formulae. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 85\u201399. Springer, Heidelberg (2001)"},{"issue":"2","key":"9_CR15","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1015071400913","volume":"28","author":"E. Giunchiglia","year":"2002","unstructured":"Giunchiglia, E., Tacchella, A., Giunchiglia, F.: SAT-based decision procedures for classical modal logics. Journal of Automated Reasoning\u00a028(2), 143\u2013171 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR16","series-title":"Lecture Notes in Artificial Intelligence","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, p. 701. Springer, Heidelberg (2001)"},{"key":"9_CR17","series-title":"165 of Synthese Library","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-94-009-6259-0_10","volume-title":"Handbook of Philosophical Logic","author":"D. Harel","year":"1984","unstructured":"Harel, D.: Dynamic logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic. 165 of Synthese Library, vol.\u00a0II, pp. 497\u2013604. D. Reidel Publishing Co., Dordrecht (1984)"},{"key":"9_CR18","unstructured":"HyLoRes\u2019 Home Page (2004), \n                  \n                    http:\/\/www.loria.fr\/~areces\/HyLoRes\/"},{"key":"9_CR19","unstructured":"Mitchell, D., Sleman, B., Levesque, H.: Hard and easy distributions of SAT problems. In: Proc. of the 10th National Conference on Artificial Intelligence, pp. 459\u2013465 (1992)"},{"issue":"2","key":"9_CR20","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0890-5401(91)90026-X","volume":"93","author":"S. Passy","year":"1991","unstructured":"Passy, S., Tinchev, T.: An essay in combinatory dynamic logic. Information and Computation\u00a093(2), 263\u2013332 (1991)","journal-title":"Information and Computation"},{"key":"9_CR21","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1613\/jair.1166","volume":"18","author":"P. Patel-Schneider","year":"2003","unstructured":"Patel-Schneider, P., Sebastiani, R.: A new general method to generate random modal formulae for testing decision procedures. Journal of Artificial Intelligence Research\u00a018, 351\u2013389 (2003)","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"2","key":"9_CR22","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications\u00a015(2), 91\u2013110 (2002) Special issue on CASC","journal-title":"AI Communications"},{"key":"9_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/3-540-45744-5_3","volume-title":"Automated Reasoning","author":"A. Voronkov","year":"2001","unstructured":"Voronkov, A.: Algorithms, datastructures, and other issues in efficient automated deduction. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 13\u201328. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32275-7_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:47:00Z","timestamp":1620013620000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32275-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540252368","9783540322757"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32275-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}