{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:14:51Z","timestamp":1725664491935},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540593386"},{"type":"electronic","value":"9783540492351"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59338-1_30","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:13:57Z","timestamp":1330276437000},"page":"95-105","source":"Crossref","is-referenced-by-count":4,"title":["Refutation systems for prepositional modal logics"],"prefix":"10.1007","author":[{"given":"Pierangelo","family":"Miglioli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ugo","family":"Moscato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Ornaghi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"7_CR1","unstructured":"Boolos G.-The unprovability of consistency-Cambridge University Press, 1979."},{"key":"7_CR2","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","volume":"LVII","author":"R. Dyckhoff","year":"1992","unstructured":"Dyckhoff R.-Contraction-free sequent calculi for intuitionistic logic-Journal of Symbolic Logic, LVII, 1992, pp. 795\u2013807.","journal-title":"Journal of Symbolic Logic"},{"key":"7_CR3","unstructured":"Fitting M.-Intuitionistic Logic, Model Theory and Forcing-North Holland, 1969."},{"key":"7_CR4","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1305\/ndjfl\/1093887933","volume":"XVIII","author":"M. Fitting","year":"1977","unstructured":"Fitting M.-A tableau system for propositional S5-Notre Dame Journal of Formal Logic, XVIII, 1977, pp. 292\u2013294.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Fitting M.-Proof methods for modal and intuitionistic logic-D. Reidel Pu. Co., 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"7_CR6","unstructured":"Girle R.-Non-looping tableau for S4-in Basin D., H\u00e4hnle R., Franh\u00f6fer B., Posegga J., Schwind C. (Eds.) Proceedings of the workshop on Theorem Proving with Analytic Tableaux and Related Methods, Marseille, France, April 28\u201330, 1993, Max-Planck Institut f\u00fcr Informatik, MPI-I-93-213, 1993, pp. 77\u201388."},{"key":"7_CR7","first-page":"223","volume":"LX","author":"A. Grzegorczyk","year":"1977","unstructured":"Grzegorczyk A.-Some relational systems and the associated topological spaces-Fundamenta mathematicae, LX, 1977, pp. 223\u2013231.","journal-title":"Fundamenta mathematicae"},{"key":"7_CR8","unstructured":"Hudelmaier J.-On contraction free sequent calculus for the modal logic S4-in Broda K., D'Agosdno M., Gor\u00e8 R., Johnson R., Reeves S. (Eds.) Proceedings of the 3rd workshop on Theorem Proving with Analytic Tableaux and Related Methods, Abingdon U.K., May 4\u20136, 1994, Imperial College of Science, Technology and Medicine TR-94\/5, 1994, pp. 105\u2013112."},{"key":"7_CR9","first-page":"109","volume":"11","author":"G. Hughes","year":"1982","unstructured":"Hughes G., Cresswell M.-K1.1 is not canonical-Bulletin of the Section of Logic of Polish Academy of Sciences, 11, 1982, pp. 109\u2013113.","journal-title":"Bulletin of the Section of Logic of Polish Academy of Sciences"},{"key":"7_CR10","unstructured":"Hughes G., Cresswell M.-A Companion to Modal Logic-Methuen & Co., 1984."},{"key":"7_CR11","doi-asserted-by":"crossref","first-page":"83","DOI":"10.2307\/2267027","volume":"X","author":"J. McKinsey","year":"1945","unstructured":"McKinsey J.-On the syntactical construction of systems of modal logic-Journal of Symbolic Logic, X, 1945, pp. 83\u201394.","journal-title":"Journal of Symbolic Logic"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BF00881949","volume":"13","author":"P. Miglioli","year":"1994","unstructured":"Miglioli P., Moscato U., Ornaghi M.-An improved refutation system for intuitionistic predicate logic-The Journal of Automated Reasoning, 13, 1994, pp. 361\u2013373.","journal-title":"The Journal of Automated Reasoning"},{"key":"7_CR13","unstructured":"Miglioli P., Moscato U., Ornaghi M.-How to avoid duplications in refutation systems for intuitionistic and Kuroda logic-in Broda K., D'Agostino M., Gor\u00e8 R., Johnson R., Reeves S. (Eds.) Proceedings of the 3rd workshop on Theorem Proving with Analytic Tableaux and Related Methods, Abingdon U.K., May 4\u20136, 1994, Imperial College of Science, Technology and Medicine TR-94\/5, 1994, pp. 169\u2013187."},{"key":"7_CR14","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/BF00249258","volume":"12","author":"W. Rautenberg","year":"1983","unstructured":"Rautenberg W.-Modal tableau calculi and interpolation-Journal of Philosophical Logic, 12, 1983, pp. 403\u2013423 (correction in Journal of Philosophical Logic, 14, 1985, p. 229).","journal-title":"Journal of Philosophical Logic"},{"key":"7_CR15","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1305\/ndjfl\/1093958621","volume":"VII","author":"N. Rescher","year":"1966","unstructured":"Rescher N.-On modal renderings of intuitionistic propositional logic-Notre Dame Journal of Formal Logic, VII, 1966, pp. 277\u2013280.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"7_CR16","unstructured":"Segerberg K.-An Essay in Classical Modal Logic \u2014 Filosofiska Studier, n. 13, Uppsala, 1971."},{"key":"7_CR17","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1305\/ndjfl\/1093957741","volume":"V","author":"B. Sobocinski","year":"1964","unstructured":"Sobocinski B.-Remarks about axiomatization of certain modal systems-Notre ame Journal of Formal Logic, V, 1964, pp. 71\u201380.","journal-title":"Notre ame Journal of Formal Logic"},{"key":"7_CR18","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1305\/ndjfl\/1093957981","volume":"V","author":"B. Sobocinski","year":"1964","unstructured":"Sobocinski B.-Family K of the non-Lewis modal systems-Notre Dame Journal of Formal Logic, V, 1964, pp. 313\u2013318.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"7_CR19","unstructured":"Wallen L.-Automated Deduction in Nonclassical Logics-MIT Press, 1989."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59338-1_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:27:09Z","timestamp":1619573229000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59338-1_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540593386","9783540492351"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-59338-1_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}