{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T10:43:52Z","timestamp":1749725032701},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540612087"},{"type":"electronic","value":"9783540683681"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61208-4_14","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:19:08Z","timestamp":1330291148000},"page":"210-225","source":"Crossref","is-referenced-by-count":39,"title":["Efficient loop-check for backward proof search in some non-classical propositional logics"],"prefix":"10.1007","author":[{"given":"Alain","family":"Heuerding","sequence":"first","affiliation":[]},{"given":"Michael","family":"Seyfried","sequence":"additional","affiliation":[]},{"given":"Heinrich","family":"Zimmermann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Brian F. Chellas. Modal logic: an introduction. Cambridge University Press, 1980.","DOI":"10.1017\/CBO9780511621192"},{"issue":"3","key":"14_CR2","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. The Journal of Symbolic Logic, 57(3):795\u2013807, 1992.","journal-title":"The Journal of Symbolic Logic"},{"key":"14_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"M. Fitting","year":"1983","unstructured":"Melvin Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht, 1983."},{"key":"14_CR4","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1093\/oso\/9780198537458.003.0006","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1","author":"M. Fitting","year":"1993","unstructured":"Melvin Fitting. Basic modal logic. In Dov M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, pages 368\u2013448. Clarendon Press, Oxford, 1993."},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"D M Gabbay. Algorithmic Proof with Diminishing Resources Part 1. In E. B\u00f6rger, editor, CSL 90, LNCS 533, pages 156\u2013173, 1991.","DOI":"10.1007\/3-540-54487-9_58"},{"key":"14_CR6","volume-title":"Technical report, TR-15-95","author":"R. Gor\u00e9","year":"1995","unstructured":"Rajeev Gor\u00e9. Tableau methods for modal and temporal logics. Technical report, TR-15-95, Automated Reasoning Project, Australian National University, Canberra, Australia, 1995. To appear in Handbook of Tableau Methods, Kluwer, 199?."},{"key":"14_CR7","volume-title":"Technical report, TR-16-95","author":"R. Gor\u00e9","year":"1995","unstructured":"Rajeev Gor\u00e9, Wolfgang Heinle, and Alain Heuerding. Relations between propositional normal modal logics: an overview. Technical report, TR-16-95, Automated Reasoning Project, Australian National University, Canberra, Australia, 1995."},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Alain Heuerding, Gerhard J\u00e4ger, Stefan Schwendimann, and Michael Seyfried. Prepositional logics on the computer. In Peter Baumgartner, Reiner H\u00e4hnle, and Joachim Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods, LNCS 918, pages 310\u2013323, 1995.","DOI":"10.1007\/3-540-59338-1_44"},{"issue":"1","key":"14_CR9","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1093\/logcom\/3.1.63","volume":"3","author":"J. Hudelmaier","year":"1993","unstructured":"J\u00f6rg Hudelmaier. An O(n log n)-space decision procedure for intuitionistic propositional logic. Journal of Logic and Computation, 3(1):63\u201375, 1993.","journal-title":"Journal of Logic and Computation"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"J\u00f6rg Hudelmaier. On a contraction free sequent calculus for the modal logic S4. In TABLEAUX 94. 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 1994.","DOI":"10.1007\/978-94-017-2798-3_1"},{"key":"14_CR11","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"S.C. Kleene. Introduction to Metamathematics. North-Holland, Amsterdam, 1952."},{"issue":"3","key":"14_CR12","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. E. Ladner","year":"1977","unstructured":"Richard E. Ladner. The computational complexity of provability in systems of modal prepositional logic. SIAM Journal on Computing, 6(3):467\u2013480, 1977.","journal-title":"SIAM Journal on Computing"},{"key":"14_CR13","unstructured":"LWBtheory. http:\/\/1wbwww.unibe.ch:8080\/LWBtheory.html, 1995."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Nicholas Rescher and Alasdair Urquhart. Temporal Logic. Springer, 1971.","DOI":"10.1007\/978-3-7091-7664-1"},{"key":"14_CR15","unstructured":"Michael Seyfried. A sequent calculus for proof search in the (\u2192, \u2227)-fragment of intuitionistic logic. Unpublished, 1994."},{"key":"14_CR16","volume-title":"Master's thesis","author":"H. Zimmermann","year":"1995","unstructured":"Heinrich Zimmermann. A directed tree calculus for minimal tense logic. Master's thesis, IAM, University of Berne, Switzerland, 1995."}],"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-61208-4_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:19:40Z","timestamp":1713633580000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61208-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540612087","9783540683681"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-61208-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}