{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T02:31:28Z","timestamp":1748399488956,"version":"3.37.3"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2022,8,30]],"date-time":"2022-08-30T00:00:00Z","timestamp":1661817600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,8,30]],"date-time":"2022-08-30T00:00:00Z","timestamp":1661817600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1007\/s11225-022-10010-9","type":"journal-article","created":{"date-parts":[[2022,8,30]],"date-time":"2022-08-30T20:05:52Z","timestamp":1661889952000},"page":"1507-1536","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Loop-Check Specification for a Sequent Calculus of Temporal Logic"],"prefix":"10.1007","volume":"110","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7792-5285","authenticated-orcid":false,"given":"Romas","family":"Alonderis","sequence":"first","affiliation":[]},{"given":"Regimantas","family":"Pliu\u0161kevi\u010dius","sequence":"additional","affiliation":[]},{"given":"Aida","family":"Pliu\u0161kevi\u010dien\u0117","sequence":"additional","affiliation":[]},{"given":"Haroldas","family":"Giedra","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,30]]},"reference":[{"key":"10010_CR1","doi-asserted-by":"crossref","unstructured":"Afshari, B., and G. E. Leigh, Cut-free completeness for modal mu-calculus, in 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland, 2017, pp. 1\u201312.","DOI":"10.1109\/LICS.2017.8005088"},{"key":"10010_CR2","doi-asserted-by":"crossref","unstructured":"Alonderis, R., R. Pliu\u0161kevi\u010dius, A. Pliu\u0161kevi\u010dien\u0117, and H. Giedra, Loop-type sequent calculi for temporal logic, Journal of Automated Reasoning 64(8):1663\u20131684, 2020.","DOI":"10.1007\/s10817-020-09544-1"},{"key":"10010_CR3","first-page":"237","volume":"52","author":"J Andrikonis","year":"2011","unstructured":"Andrikonis, J., and R. Pliu\u0161kevi\u010dius, Contraction-free calculi for modal logics S5 and KD45, Lietuvos matematikos rinkinys, LMD darbai 52:237\u2013242, 2011.","journal-title":"Lietuvos matematikos rinkinys, LMD darbai"},{"issue":"1","key":"10010_CR4","first-page":"40","volume":"6","author":"IN Brodsky","year":"1988","unstructured":"Brodsky, I. N., Enthymeme reconstruction, Bulletin of Leningrad State University 6(1):40\u201344, 1988.","journal-title":"Bulletin of Leningrad State University"},{"key":"10010_CR5","doi-asserted-by":"publisher","unstructured":"Brotherston, J., Cyclic proofs for first-order logic with inductive definitions, in TABLEAUX, vol. 3702 of Lecture Notes in Artificial Intelligence, Springer Verlag, 2005, pp. 78\u201392. https:\/\/doi.org\/10.1007\/11554554_8.","DOI":"10.1007\/11554554_8"},{"issue":"2","key":"10010_CR6","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1016\/j.jlap.2008.02.004","volume":"76","author":"K Br\u00fcnnler","year":"2008","unstructured":"Br\u00fcnnler, K., and M. Lange, Cut-free sequent systems for temporal logic, The Journal of Logic and Algebraic Programming 76(2):216\u2013225, 2008.","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"10010_CR7","doi-asserted-by":"crossref","unstructured":"Das, A., and D. Pous, A cut-free cyclic proof system for kleene algebra, in R.A. Schmidt, and C. Nalon, (eds.), Automated Reasoning with Analytic Tableaux and Related Methods\u201326th International Conference, TABLEAUX 2017, Bras\u00edlia, Brazil, September 25\u201328, 2017, Proceedings, vol. 10501 of Lecture Notes in Computer Science, Springer, 2017, pp. 261\u2013277.","DOI":"10.1007\/978-3-319-66902-1_16"},{"key":"10010_CR8","doi-asserted-by":"crossref","unstructured":"Dax, C., M. Hofmann, and M. Lange, A proof system for the linear time $$\\mu $$-Calculus, in S. Arun-Kumar, and N. Garg, (eds.), FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, vol. 4337 of Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 2006, pp. 273\u2013284.","DOI":"10.1007\/11944836_26"},{"issue":"3","key":"10010_CR9","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R Dyckhoff","year":"1992","unstructured":"Dyckhoff, R., 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":"10010_CR10","doi-asserted-by":"publisher","unstructured":"Hazard, E., and D. Kuperberg, Cyclic proofs for transfinite expressions, in F. Manea, and A. Simpson, (eds.), 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), vol. 216 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 2022, pp. 23:1\u201323:18. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2022.23","DOI":"10.4230\/LIPIcs.CSL.2022.23"},{"key":"10010_CR11","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/3-540-61208-4_14","volume":"1071","author":"A Heuerding","year":"1996","unstructured":"Heuerding, A., M. Seyfried, and H. Zimmermann, Efficient loop-check for backward proof search in some non-classical propositional logics, Lecture Notes in Computer Science 1071:210\u2013225, 1996.","journal-title":"Lecture Notes in Computer Science"},{"key":"10010_CR12","doi-asserted-by":"crossref","unstructured":"Hudelmaier, J., A contraction-free sequent calculus for S4, in H. Wansing, (ed.), Proof Theory of Modal Logic, Kluwer Academic Publishers, 1996, pp. 3\u201315.","DOI":"10.1007\/978-94-017-2798-3_1"},{"key":"10010_CR13","doi-asserted-by":"crossref","unstructured":"Kokkinis, I., and T. Studer, Cyclic proofs for linear temporal logic, in D. Probst, and P. Schuster, (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science, vol. 6 of Ontos Mathematical Logic, De Gruyter, 2016, pp. 171\u2013192.","DOI":"10.1515\/9781501502620-011"},{"key":"10010_CR14","unstructured":"Moukhachjov, V. P., and I. V. Netchitailov, An improvement of Brodsky\u2019s coding method for the sequent calculus of first-order logic, in Logic Joint International Conference of Automated Reasoning, Siena, Italy, 18\u201325 June, 2001, pp. 113\u2013121."},{"key":"10010_CR15","doi-asserted-by":"crossref","unstructured":"Nide, N., and S. Takata, Deduction systems for BDI logic using sequent calculus, in AAMAS \u201902: Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, Association for Computing Machinery, New York, 2002, pp. 928\u2013935.","DOI":"10.1145\/544862.544955"},{"key":"10010_CR16","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/BFb0026305","volume":"385","author":"B Paech","year":"1988","unstructured":"Paech, B., Gentzen-systems for propositional temporal logics, Lecture Notes in Computer Science 385:240\u2013253, 1988.","journal-title":"Lecture Notes in Computer Science"},{"key":"10010_CR17","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/BFb0029643","volume":"452","author":"R Pliu\u0161kevi\u010dius","year":"1990","unstructured":"Pliu\u0161kevi\u010dius, R., Investigation of fininitary calculi for temporal logics by means on infinitary calculi, Lecture Notes in Computer Science 452:464\u2013469, 1990.","journal-title":"Lecture Notes in Computer Science"},{"key":"10010_CR18","first-page":"413","volume":"41","author":"A Pliu\u0161kevi\u010dien\u0117","year":"2001","unstructured":"Pliu\u0161kevi\u010dien\u0117, A., Decision procedure for a fragment of dynamic logic, Lithuanian Mathematical Journal, special issue 41:\u00a0413\u2013420, 2001.","journal-title":"Lith. Math. Journal, special issue"},{"key":"10010_CR19","first-page":"112","volume":"3900","author":"R Pliu\u0161kevi\u010dius","year":"2006","unstructured":"Pliu\u0161kevi\u010dius, R., and A. Pliu\u0161kevi\u010dien\u0117, Decision procedure for a fragment of mutual belief logic with quantified agent variables, Lecture Notes in Artificial Intelligence 3900:112\u2013128, 2006.","journal-title":"Lecture Notes in Artificial Intelligence"},{"key":"10010_CR20","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1111\/j.1755-2567.1977.tb00778.x","volume":"43","author":"G Sundholm","year":"1977","unstructured":"Sundholm, G., A completeness proof for an infinitary tense-logic, Theoria 43:47\u201351, 1977. https:\/\/doi.org\/10.1111\/j.1755-2567.1977.tb00778.x","journal-title":"Theoria"},{"key":"10010_CR21","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1007\/s10817-019-09532-0","volume":"64","author":"G Tellez","year":"2020","unstructured":"Tellez, G., and J. Brotherston, Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof, Journal of Automated Reasoning 64:555\u2013578, 2020. https:\/\/doi.org\/10.1007\/s10817-019-09532-0","journal-title":"J Autom Reasoning"},{"key":"10010_CR22","first-page":"119","volume":"28","author":"P Wolper","year":"1985","unstructured":"Wolper, P., The tableau method for temporal logic: An overview, Logique et Analyse 28:119\u2013136, 1985.","journal-title":"Logique et Analyse"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-022-10010-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-022-10010-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-022-10010-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,2]],"date-time":"2024-10-02T21:16:33Z","timestamp":1727903793000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-022-10010-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,30]]},"references-count":22,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["10010"],"URL":"https:\/\/doi.org\/10.1007\/s11225-022-10010-9","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2022,8,30]]},"assertion":[{"value":"20 January 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 June 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 August 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}