{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:22Z","timestamp":1759017922076,"version":"3.44.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032060846","type":"print"},{"value":"9783032060853","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The first algorithm to transform a proof in Nishimura\u2019s sequent calculus <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textbf{GKt}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>GKt<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> for tense logic <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textbf{Kt}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>Kt<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> into an analytic proof of the same sequent is presented. In an analytic proof, every rule instance is analytic i.e., each formula in every premise is a subformula of some formula in its conclusion. We call this algorithm <jats:italic>analytic restriction<\/jats:italic> to convey that it extends analytic cut-restriction where just the cut-rule instances are made analytic. This distinction is essential in tense logic since cut and modal rules can both cause non-analyticity. Analytic cut-restriction is itself an extension of cut-elimination\u00a0so our work contributes to a broader program of transforming arbitrary sequent proofs into ones constructed from a designated set of formulas\u2014not necessarily subformulas. As with cut-elimination, the aim is to limit the proof search space and support proof-theoretic and meta-logical investigations.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_12","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:20Z","timestamp":1758969920000},"page":"220-237","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Analytic Proofs for\u00a0Tense Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6947-8772","authenticated-orcid":false,"given":"Agata","family":"Ciabattoni","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8257-968X","authenticated-orcid":false,"given":"Timo","family":"Lang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7940-9065","authenticated-orcid":false,"given":"Revantha","family":"Ramanayake","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics. In: Logic: From Foundations to Applications (Staffordshire, 1993), pp. 1\u201332. Oxford Univ. Press, New York (1996)","DOI":"10.1093\/oso\/9780198538622.003.0001"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Avron, A., Lahav, O.: A unified semantic framework for fully structural propositional sequent systems. ACM Trans. Comput. Log. 14(4) (2013)","DOI":"10.1145\/2528930"},{"issue":"4","key":"12_CR3","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/BF00284976","volume":"11","author":"ND Belnap","year":"1982","unstructured":"Belnap, N.D.: Display logic. J. Philos. Log. 11(4), 375\u2013417 (1982)","journal-title":"J. Philos. Log."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Blackburn, P., de Rijke, M., Venema, I.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge (2001)","DOI":"10.1017\/CBO9781107050884"},{"issue":"2","key":"12_CR5","doi-asserted-by":"publisher","first-page":"635","DOI":"10.1017\/jsl.2021.42","volume":"86","author":"A Ciabattoni","year":"2021","unstructured":"Ciabattoni, A., Lang, T., Ramanayake, R.: Bounded-analytic sequent calculi and embeddings for hypersequent logics. J. Symb. Log. 86(2), 635\u2013668 (2021)","journal-title":"J. Symb. Log."},{"key":"12_CR6","doi-asserted-by":"publisher","unstructured":"Ciabattoni, A., Lang, T., Ramanayake, R.: Cut-restriction: From cuts to analytic cuts. In: 38th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, 26\u201329 June 2023, pp. 1\u201313. IEEE (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175785","DOI":"10.1109\/LICS56636.2023.10175785"},{"key":"12_CR7","unstructured":"Ciabattoni, A., Olivetti, N., Parent, X., Ramanayake, R., Rozplokhas, D.: Analytic proof theory for \u00e5qvist\u2019s system F. In: Maranh\u00e3o, J., Peterson, C., Stra\u00dfer, C., van\u00a0der Torre, L. (eds.) Deontic Logic and Normative Systems - 16th International Conference, DEON 2023, Trois-Rivi\u00e8res, QC, Canada, 5\u20137 July 2023, pp. 79\u201398. College Publications (2023)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"D\u2019Agostino, M., Mondadori, M.: The taming of the cut. Classical refutations with analytic cut. J. Log. Comput. 4, 285\u2013319 (1994)","DOI":"10.1093\/logcom\/4.3.285"},{"key":"12_CR9","unstructured":"Belardinelli, F., Jipsen, P., Ono, H.: Algebraic aspects of cut elimination. Stud. Log. 68, 1\u201332 (2001)"},{"issue":"4","key":"12_CR10","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/BF02176170","volume":"37","author":"M Fitting","year":"1978","unstructured":"Fitting, M.: Subformula results in some propositional modal logics. Stud. Log. 37(4), 387\u2013391 (1978)","journal-title":"Stud. Log."},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Gabbay, D.: Labelled Deductive Systems, vol. 1\u2014Foundations. Oxford University Press, Oxford (1996)","DOI":"10.1093\/oso\/9780198538332.003.0001"},{"key":"12_CR12","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen 39, 176\u2013210, 405\u2013431 (1934\/35). english translation in: American Philosophical Quarterly 1 (1964), 288\u2013306 and American Philosophical Quarterly 2 (1965), 204\u2013218, as well as in: The Collected Papers of Gerhard Gentzen, (ed. M.E. Szabo), pp. 68\u2013131. Amsterdam, North Holland (1969)"},{"key":"12_CR13","unstructured":"Girard, J.Y.: Proof Theory and Logical Complexity, Studies in Proof Theory. Monographs, vol.\u00a01. Bibliopolis, Naples (1987)"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Gor\u00e9, R., Postniece, L., Tiu, A.: On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Log. Methods Comput. Sci. 7(2), 2:8, 38 (2011)","DOI":"10.2168\/LMCS-7(2:8)2011"},{"issue":"2","key":"12_CR15","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1017\/S1755020311000323","volume":"5","author":"R Gor\u00e9","year":"2012","unstructured":"Gor\u00e9, R., Ramanayake, R.: Valentini\u2019s cut-elimination for provability logic resolved. Rev. Symb. Log. 5(2), 212\u2013238 (2012)","journal-title":"Rev. Symb. Log."},{"issue":"4","key":"12_CR16","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1017\/S1755020319000352","volume":"12","author":"A Indrzejczak","year":"2019","unstructured":"Indrzejczak, A.: Cut elimination in hypersequent calculus for some logics of linear time. Rev. Symb. Log. 12(4), 806\u2013822 (2019)","journal-title":"Rev. Symb. Log."},{"issue":"2","key":"12_CR17","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1017\/S175502031600040X","volume":"10","author":"T Kowalski","year":"2017","unstructured":"Kowalski, T., Ono, H.: Analytic cut and interpolation for bi-intuitionistic logic. Rev. Symb. Log. 10(2), 259\u2013283 (2017)","journal-title":"Rev. Symb. Log."},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Kracht, M.: Power and weakness of the modal display calculus. In: Proof Theory of Modal Logic (Hamburg, 1993), Appl. Log. Ser., vol.\u00a02, pp. 93\u2013121. Kluwer Acad. Publ., Dordrecht (1996)","DOI":"10.1007\/978-94-017-2798-3_7"},{"issue":"5\u20136","key":"12_CR19","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","volume":"34","author":"S Negri","year":"2005","unstructured":"Negri, S.: Proof analysis in modal logic. J. Philos. Log. 34(5\u20136), 507\u2013544 (2005)","journal-title":"J. Philos. Log."},{"issue":"2","key":"12_CR20","doi-asserted-by":"publisher","first-page":"343","DOI":"10.2977\/prims\/1195187208","volume":"16","author":"H Nishimura","year":"1980","unstructured":"Nishimura, H.: A study of some tense logics by gentzen\u2019s sequential method. Publ. Res. Inst. Math. Sci. 16(2), 343\u2013353 (1980)","journal-title":"Publ. Res. Inst. Math. Sci."},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"560","DOI":"10.2307\/2271362","volume":"33","author":"RM Smullyan","year":"1968","unstructured":"Smullyan, R.M.: Analytic cut. J. Symb. Log. 33, 560\u2013564 (1968)","journal-title":"J. Symb. Log."},{"key":"12_CR22","first-page":"1129","volume":"37","author":"M Takano","year":"1992","unstructured":"Takano, M.: Subformula property as a substitute for cut-elimination in modal propositional logics. Math. Japon. 37, 1129\u20131145 (1992)","journal-title":"Math. Japon."},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Takano, M.: A modified subformula property for the modal logics K5 and K5D. Bull. Sect. Log. 30 (2001). https:\/\/doi.org\/10.18778\/0138-0680.48.1.02","DOI":"10.18778\/0138-0680.48.1.02"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Terui, K.: Which structural rules admit cut elimination? An algebraic criterion. J. Symb. Log. 72(3), 738\u2013754 (2007)","DOI":"10.2178\/jsl\/1191333839"},{"key":"12_CR25","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, vol. 43, second edn. Cambridge University Press, Cambridge (2000)"},{"issue":"4","key":"12_CR26","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/BF00249262","volume":"12","author":"S Valentini","year":"1983","unstructured":"Valentini, S.: The modal logic of provability: cut-elimination. J. Philos. Log. 12(4), 471\u2013476 (1983)","journal-title":"J. Philos. Log."},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Valentini, S.: A syntactic proof of cut-elimination for $${\\rm gl}_{{\\rm lin}}$$. Z. Math. Logik Grundlag. Math. 32(2), 137\u2013144 (1986)","DOI":"10.1002\/malq.19860320707"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Vigan\u00f2, L.: Labelled Non-Classical Logics. Kluwer Academic Publishers, Dordrecht (2000). with a foreword by Dov M. Gabbay","DOI":"10.1007\/978-1-4757-3208-5"},{"key":"12_CR29","doi-asserted-by":"publisher","unstructured":"Wansing, H.: Displaying Modal Logic, Trends in Logic. Springer, Cham (1998). https:\/\/doi.org\/10.1007\/978-94-017-1280-4","DOI":"10.1007\/978-94-017-1280-4"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06085-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:24Z","timestamp":1758969924000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/tableaux\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}