{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T15:27:05Z","timestamp":1720625225021},"reference-count":20,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2011,11,1]],"date-time":"2011-11-01T00:00:00Z","timestamp":1320105600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":636,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2011,11]]},"DOI":"10.1016\/j.entcs.2011.10.002","type":"journal-article","created":{"date-parts":[[2011,10,31]],"date-time":"2011-10-31T08:30:54Z","timestamp":1320049854000},"page":"3-16","source":"Crossref","is-referenced-by-count":2,"special_numbering":"C","title":["Unsorted Functional Translations"],"prefix":"10.1016","volume":"278","author":[{"given":"Carlos","family":"Areces","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Gor\u00edn","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2011.10.002_br0010","unstructured":"C. Areces, R. Gennari, J. Heguiabere, and M. de Rijke. Tree-based heuristics in modal theorem proving. In Proc. of ECAI\u02bc2000, pages 199\u2013203, 2000."},{"key":"10.1016\/j.entcs.2011.10.002_br0020","first-page":"821","article-title":"Hybrid logics","author":"Areces","year":"2006"},{"key":"10.1016\/j.entcs.2011.10.002_br0030","series-title":"Proc. of the 11th IJCAI","first-page":"441","article-title":"Modal theorem proving: An equational viewpoint","author":"Auffray","year":"1989"},{"issue":"3","key":"10.1016\/j.entcs.2011.10.002_br0040","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","volume":"2","author":"Auffray","year":"1992","journal-title":"J. of Logic and Computation"},{"key":"10.1016\/j.entcs.2011.10.002_br0050","series-title":"Modal Logic","author":"Blackburn","year":"2002"},{"key":"10.1016\/j.entcs.2011.10.002_br0060","series-title":"Proc. of CADE-9","first-page":"487","article-title":"Linear modal deductions","volume":"vol. 310","author":"Fari\u00f1as del Cerro","year":"1988"},{"key":"10.1016\/j.entcs.2011.10.002_br0070","series-title":"Algebra and Logic","first-page":"163","article-title":"Axiomatic classes in propositional modal logic","volume":"vol. 450","author":"Goldblatt","year":"1975"},{"key":"10.1016\/j.entcs.2011.10.002_br0080","unstructured":"D. Gor\u00edn. Automated reasoning techniques for hybrid logics. PhD thesis, Universidad de Buenos and Universit\u00e9 Henri Poincar\u00e9, 2009."},{"key":"10.1016\/j.entcs.2011.10.002_br0090","first-page":"181","article-title":"Computational modal logic","author":"Horrocks","year":"2006"},{"issue":"4","key":"10.1016\/j.entcs.2011.10.002_br0100","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1080\/11663081.1999.10510981","article-title":"An empirical analysis of modal theorem provers","volume":"9","author":"Hustadt","year":"1999","journal-title":"J. of Applied Non-Classical Logics"},{"issue":"3","key":"10.1016\/j.entcs.2011.10.002_br0110","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1145\/321958.321960","article-title":"Resolution strategies as decision procedures","volume":"23","author":"Joyner","year":"1976","journal-title":"J. of the ACM"},{"key":"10.1016\/j.entcs.2011.10.002_br0120","unstructured":"H. Ohlbach. A Resolution Calculus for Modal Logics. PhD thesis, Universit\u00e4t Kaiserslautern, 1988."},{"key":"10.1016\/j.entcs.2011.10.002_br0130","series-title":"Proc. of CADE-9","first-page":"500","article-title":"A resolution calculus for modal logics","volume":"vol. 310","author":"Ohlbach","year":"1988"},{"issue":"5","key":"10.1016\/j.entcs.2011.10.002_br0140","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1093\/logcom\/7.5.581","article-title":"Functional translation and second-order frame properties of modal logics","volume":"7","author":"Ohlbach","year":"1997","journal-title":"J. of Logic and Computation"},{"key":"10.1016\/j.entcs.2011.10.002_br0150","unstructured":"R. Schmidt. Optimised Modal Translation and Resolution. PhD thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, 1997."},{"issue":"4","key":"10.1016\/j.entcs.2011.10.002_br0160","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1023\/A:1006043519663","article-title":"Decidability by resolution for propositional modal logics","volume":"22","author":"Schmidt","year":"1999","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/j.entcs.2011.10.002_br0170","series-title":"Sorts and Types in Artificial Intelligence","first-page":"18","article-title":"Many-sorted inferences in automated theorem proving","volume":"vol. 418","author":"Walther","year":"1989"},{"key":"10.1016\/j.entcs.2011.10.002_br0180","first-page":"1965","article-title":"Combining superposition, sorts and splitting","volume":"vol. 2","author":"Weidenbach","year":"2001"},{"key":"10.1016\/j.entcs.2011.10.002_br0190","series-title":"Proc. of CADE-21","first-page":"514","article-title":"System description: Spass version 3.0","volume":"vol. 4603","author":"Weidenbach","year":"2007"},{"issue":"9","key":"10.1016\/j.entcs.2011.10.002_br0200","first-page":"23","article-title":"Modal resolutions","volume":"33","author":"Zamov","year":"1989","journal-title":"Soviet Math"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066111001307?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066111001307?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,11,29]],"date-time":"2018-11-29T02:52:07Z","timestamp":1543459927000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066111001307"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11]]},"references-count":20,"alternative-id":["S1571066111001307"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2011.10.002","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2011,11]]}}}