{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:17Z","timestamp":1725494297996},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_2","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T20:53:07Z","timestamp":1194641587000},"page":"16-30","source":"Crossref","is-referenced-by-count":1,"title":["Tractable Transformations from Modal Provability Logics into First-Order Logic"],"prefix":"10.1007","author":[{"given":"St\u00e9ephane","family":"Demri","sequence":"first","affiliation":[]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00302639","volume":"6","author":"Y. Auffray","year":"1990","unstructured":"Y. Auffray, P. Enjalbert, and J.-J. Herbrard. Strategies for modal resolution: results and problems. Journal of Automated Reasoning, 6:1\u201338, 1990.","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"2_CR2","doi-asserted-by":"publisher","first-page":"935","DOI":"10.2307\/2274147","volume":"49","author":"A. Avron","year":"1984","unstructured":"A. Avron. On modal systems having arithmetical interpretations. Journal of Symbolic Logic, 49(3):935\u2013942, 1984.","journal-title":"Journal of Symbolic Logic"},{"key":"2_CR3","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF00284976","volume":"11","author":"N. Belnap","year":"1982","unstructured":"N. Belnap. Display logic. Journal of Philosophical Logic, 11:375\u2013417, 1982.","journal-title":"Journal of Philosophical Logic"},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1002\/malq.19860321002","volume":"32","author":"M. Borga","year":"1986","unstructured":"M. Borga and P. Gentilini. On the proof theory of the modal logic Grz. Zeitschrift f\u00fcur Mathematik Logik und Grundlagen der Mathematik, 32:145\u2013148, 1986.","journal-title":"Zeitschrift f\u00fcur Mathematik Logik und Grundlagen der Mathematik"},{"key":"2_CR5","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1080\/11663081.1994.10510818","volume":"4","author":"Ph. Balbiani","year":"1994","unstructured":"Ph. Balbiani and A. Herzig. A translation from the modal logic of provability into K4. Journal of Applied Non-Classical Logics, 4:73\u201377, 1994.","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"G. Boolos. The Logic of Provability. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511625183"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"S. Demri and R. Gor\u00e9. An O((n.log n)3)-time transformation from Grz into decidable fragments of classical first-order logic. In Selected papers of FTP\u201998, Vienna. LNAI, Springer-Verlag, 1999. to appear.","DOI":"10.1007\/3-540-46508-1_10"},{"key":"2_CR8","unstructured":"S. Demri and R. Gor\u00e9. Theoremhood preserving maps as a characterisation of cut elimination for provability logics. Technical report, A.R.P., A.N.U., 1999. Forthcoming."},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/BF00881803","volume":"15","author":"G. d\u2019Agostino","year":"1995","unstructured":"G. d\u2019Agostino, A. Montanari, and A. Policriti. A set-theoretical translation method for polymodal logics. Journal of Automated Reasoning, 15:317\u2013337, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"M. Fitting. Proof methods for modal and intuitionistic logics. D. Reidel Publishing Co., 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"2_CR11","unstructured":"H. Ganzinger, U. Hustadt, and R. Meyer, C. Schmidt. A resolution-based decision procedure for extensions of K4. In 2nd Workshop on Advances in Modal Logic (AiML\u201998), Uppsala, Sweden, October 1998. to appear."},{"key":"2_CR12","volume-title":"Handbook of Tableaux Methods","author":"R. Gor\u00e9","year":"1999","unstructured":"R. Gor\u00e9.Tableaux methods for modal and temporal logics. In M. d\u2019Agostino, D. Gabbay, R. H\u00e4hnle, and J. Posegga, editors, Handbook of Tableaux Methods. Kluwer, Dordrecht, 1999. To appear."},{"key":"2_CR13","volume-title":"Raisonnement automatique en logique modale et algorithmes d\u2019unification","author":"A. Herzig","year":"1989","unstructured":"A. Herzig. Raisonnement automatique en logique modale et algorithmes d\u2019unification. PhD thesis, Universit\u00e9 P. Sabatier, Toulouse, 1989."},{"key":"2_CR14","unstructured":"U. Hustadt and R. Schmidt. On evaluating decision procedures for modal logic. In IJCAI-15, pages 202\u2013207. Morgan Kaufmann, 1997."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"M. Kracht. Power and weakness of the modal display calculus. In H. Wansing, editor, Proof theory of modal logic, pages 93\u2013121. Kluwer Academic Publishers, 1996.","DOI":"10.1007\/978-94-017-2798-3_7"},{"issue":"3","key":"2_CR16","doi-asserted-by":"publisher","first-page":"531","DOI":"10.2307\/2273755","volume":"46","author":"D. Leivant","year":"1981","unstructured":"D. Leivant. On the proof theory of the modal logic for arithmetical provability. Journal of Symbolic Logic, 46(3):531\u2013538, 1981.","journal-title":"Journal of Symbolic Logic"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"F. Massacci. Strongly analytic tableaux for normal modal logics. In A. Bundy, editor, CADE-12, pages 723\u2013737. LNAI 814, July 1994.","DOI":"10.1007\/3-540-58156-1_52"},{"key":"2_CR18","series-title":"Lect Notes Comput Sci","first-page":"198","volume-title":"International Conference on Computer Logic, Tallinn","author":"G. Mints","year":"1988","unstructured":"G. Mints. Gentzen-type and resolution rules part I: propositional logic. In P. Martin-L\u00f6f and G. Mints, editors, International Conference on Computer Logic, Tallinn, pages 198\u2013231. LNCS 417, 1988."},{"issue":"8","key":"2_CR19","doi-asserted-by":"publisher","first-page":"852","DOI":"10.1109\/TC.1976.1674704","volume":"25","author":"Ch. Morgan","year":"1976","unstructured":"Ch. Morgan. Methods for automated theorem proving in non classical logics. IEEE Transactions on Computers, 25(8):852\u2013862, 1976.","journal-title":"IEEE Transactions on Computers"},{"key":"2_CR20","unstructured":"A. Nonnengart and A. Szalas. A fixpoint approach to second-order quantifier elimination with applications to correspondence theory. In E. Or lowska, editor, Logic at Work. Essays Dedicated to the Memory of Helena Rasiowa, pages 89\u2013108. Physica Verlag, 1998."},{"key":"2_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"500","DOI":"10.1007\/BFb0012852","volume-title":"CADE-9","author":"H.J. Ohlbach","year":"1988","unstructured":"H.J. Ohlbach. A resolution calculus for modal logics. In CADE-9, pages 500\u2013516. LNCS 310, 1988."},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"H.J. Ohlbach. Combining Hilbert style and semantic reasoning in a resolution framework. In C. Kirchner and H. Kirchner, editors, CADE-15, Lindau, Germany, pages 205\u2013219. LNAI 1421, 1998.","DOI":"10.1007\/BFb0054261"},{"key":"2_CR23","unstructured":"Ch. Papadimitriou. Computational Complexity. Addison-Wesley Publishing Company, 1994."},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logics. In S. Kanger, editor, 3rd Scandinavian Logic Symposium, pages 110\u2013143. North Holland, 1975.","DOI":"10.1016\/S0049-237X(08)70728-6"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"R. Schmidt. Decidability by resolution for propositional modal logics. Journal of Automated Reasoning, 1999. To appear.","DOI":"10.1023\/A:1006043519663"},{"key":"2_CR26","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/BF00370323","volume":"39","author":"G. Sambin","year":"1980","unstructured":"G. Sambin and S. Valentini. A modal sequent calculus for a fragment of arithmetic. Studia Logica, 39:245\u2013256, 1980.","journal-title":"Studia Logica"},{"key":"2_CR27","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BF00293433","volume":"11","author":"G. Sambin","year":"1982","unstructured":"G. Sambin and S. Valentini. The modal logic of provability. The sequential approach. Journal of Philosophical Logic, 11:311\u2013342, 1982.","journal-title":"Journal of Philosophical Logic"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/BF00249262","volume":"12","author":"S. Valentini","year":"1983","unstructured":"S. Valentini. The modal logic of provability: cut-elimination. Journal of Philosophical Logic, 12:471\u2013476, 1983.","journal-title":"Journal of Philosophical Logic"},{"issue":"2","key":"2_CR29","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1093\/logcom\/4.2.125","volume":"4","author":"H. Wansing","year":"1994","unstructured":"H. Wansing. Sequent calculi for normal modal propositional logics. Journal of Logic and Computation, 4(2):125\u2013142, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"2_CR30","volume-title":"Trends in Logic","author":"H. Wansing","year":"1998","unstructured":"H. Wansing. Displaying Modal Logic, volume 3 of Trends in Logic. Kluwer Academic Publishers, Dordrecht, 1998."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,28]],"date-time":"2020-04-28T00:30:43Z","timestamp":1588033843000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}