{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T16:02:52Z","timestamp":1765123372026,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031635007"},{"type":"electronic","value":"9783031635014"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,2]],"date-time":"2024-07-02T00:00:00Z","timestamp":1719878400000},"content-version":"vor","delay-in-days":183,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Guarded Kleene Algebra with Tests (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt{GKAT}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>GKAT<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following earlier work by Das and Pous on Kleene Algebra, we study <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt{GKAT}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>GKAT<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> from a proof-theoretical perspective. The deterministic nature of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt{GKAT}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>GKAT<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> allows for a non-well-founded sequent system whose set of regular proofs is complete with respect to the guarded language model. This is unlike the situation with Kleene Algebra, where hypersequents are required. Moreover, the decision procedure induced by proof search runs in <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{NLOGSPACE}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>NLOGSPACE<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, whereas that of Kleene Algebra is in <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{PSPACE}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>PSPACE<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>.<\/jats:p>","DOI":"10.1007\/978-3-031-63501-4_14","type":"book-chapter","created":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:02:00Z","timestamp":1719824520000},"page":"257-275","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Cyclic Proof System for\u00a0Guarded Kleene Algebra with\u00a0Tests"],"prefix":"10.1007","author":[{"given":"Jan","family":"Rooduijn","sequence":"first","affiliation":[]},{"given":"Dexter","family":"Kozen","sequence":"additional","affiliation":[]},{"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,2]]},"reference":[{"key":"14_CR1","unstructured":"Acclavio, M., Curzi, G., Guerrieri, G.: Infinitary cut-elimination via finite approximations. In: 32nd Annual Conference on Computer Science Logic, CSL. LIPIcs, vol.\u00a0288, pp. 8:1\u20138:19. Schloss Dagstuhl (2024)"},{"issue":"1","key":"14_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/jigpal\/jzac053","volume":"32","author":"B Afshari","year":"2022","unstructured":"Afshari, B., Enqvist, S., Leigh, G.E.: Cyclic proofs for the first-order $$\\mu $$-calculus. Log. J. IGPL 32(1), 1\u201334 (2022)","journal-title":"Log. J. IGPL"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-030-86059-2_20","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"B Afshari","year":"2021","unstructured":"Afshari, B., Leigh, G.E., Men\u00e9ndez Turata, G.: Uniform interpolation from cyclic proofs: the case of modal mu-calculus. In: Das, A., Negri, S. (eds.) TABLEAUX 2021. LNCS (LNAI), vol. 12842, pp. 335\u2013353. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_20"},{"key":"14_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-031-15298-6_20","volume-title":"WoLLIC 2022","author":"B Afshari","year":"2022","unstructured":"Afshari, B., Wehr, D.: Abstract cyclic proofs. In: Ciabattoni, A., Pimentel, E., de Queiroz, R.J.G.B. (eds.) WoLLIC 2022. LNCS, vol. 13468, pp. 309\u2013325. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15298-6_20"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/11554554_8","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J Brotherston","year":"2005","unstructured":"Brotherston, J.: Cyclic proofs for first-order logic with inductive definitions. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 78\u201392. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11554554_8"},{"key":"14_CR6","unstructured":"Das, A., Doumane, A., Pous, D.: Left-handed completeness for Kleene algebra, via cyclic proofs. In: 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR. EPiC Series in Computing, vol.\u00a057, pp. 271\u2013289 (2018)"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-66902-1_16","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A Das","year":"2017","unstructured":"Das, A., Pous, D.: A cut-free cyclic proof system for Kleene algebra. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS (LNAI), vol. 10501, pp. 261\u2013277. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66902-1_16"},{"key":"14_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-031-43513-3_14","volume-title":"TABLEAUX 2023","author":"M Dekker","year":"2023","unstructured":"Dekker, M., Kloibhofer, J., Marti, J., Venema, Y.: Proof systems for the modal $$\\mu $$-calculus obtained by determinizing automata. In: Ramanayake, R., Urban, J. (eds.) TABLEAUX 2023. LNCS, vol. 14278, pp. 242\u2013259. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43513-3_14"},{"issue":"2","key":"14_CR9","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D Kozen","year":"1994","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366\u2013390 (1994)","journal-title":"Inf. Comput."},{"issue":"3","key":"14_CR10","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427\u2013443 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Nonlocal flow of control and Kleene algebra with tests. In: 23rd Annual Symposium on Logic in Computer Science, LICS, pp. 105\u2013117. IEEE (2008)","DOI":"10.1109\/LICS.2008.32"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-540-70594-9_11","volume-title":"Mathematics of Program Construction","author":"D Kozen","year":"2008","unstructured":"Kozen, D., Tseng, W.-L.D.: The B\u00f6hm\u2013Jacopini theorem is false, propositionally. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 177\u2013192. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70594-9_11"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Kuperberg, D., Pinault, L., Pous, D.: Cyclic proofs, system T, and the power of contraction. In: 48th Annual Symposium on Principles of Programming Languages, POPL, pp. 1\u201328 (2021)","DOI":"10.1145\/3434282"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Marti, J., Venema, Y.: Focus-style proof systems and interpolation for the alternation-free $$\\mu $$-calculus, arXiv preprint arXiv:2103.01671 (2021)","DOI":"10.1007\/978-3-030-86059-2_22"},{"key":"14_CR15","unstructured":"Rooduijn, J., Kozen, D., Silva, A.: A cyclic proof system for Guarded Kleene Algebra with Tests (full version) (2024). https:\/\/arxiv.org\/abs\/2405.07505"},{"key":"14_CR16","unstructured":"Rooduijn, J.: Fragments & Frame Classes. Ph.D. thesis, University of Amsterdam (2024)"},{"key":"14_CR17","unstructured":"Rozowski, W., Kapp\u00e9, T., Kozen, D., Schmid, T., Silva, A.: Probabilistic guarded KAT modulo bisimilarity: completeness and complexity. In: 50th International Colloquium on Automata, Languages, and Programming, ICALP. LIPIcs, vol.\u00a0261, pp. 136:1\u2013136:20. Schloss Dagstuhl (2023)"},{"issue":"1","key":"14_CR18","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1145\/321312.321326","volume":"13","author":"A Salomaa","year":"1966","unstructured":"Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158\u2013169 (1966)","journal-title":"J. ACM"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-662-55386-2_23","volume-title":"Logic, Language, Information, and Computation","author":"Y Savateev","year":"2017","unstructured":"Savateev, Y., Shamkanov, D.: Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs. In: Kennedy, J., de Queiroz, R.J.G.B. (eds.) WoLLIC 2017. LNCS, vol. 10388, pp. 321\u2013335. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-55386-2_23"},{"key":"14_CR20","unstructured":"Schmid, T., Kapp\u00e9, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: coequations, coinduction, and completeness. In: 48th International Colloquium on Automata, Languages, and Programming, ICALP. LIPIcs, vol.\u00a0198, pp. 142:1\u2013142:14. Schloss Dagstuhl (2021)"},{"key":"14_CR21","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-031-30044-8_12","volume-title":"ESOP 2023","author":"T Schmid","year":"2023","unstructured":"Schmid, T., Kapp\u00e9, T., Silva, A.: A complete inference system for skip-free guarded Kleene algebra with tests. In: Wies, T. (ed.) ESOP 2023. LNCS, vol. 13990, pp. 309\u2013336. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30044-8_12"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Smolka, S., Foster, N., Hsu, J., Kapp\u00e9, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. In: 47th Annual Symposium on Principles of Programming Languages, POPL, pp. 61:1\u201361:28 (2020)","DOI":"10.1145\/3371129"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/3-540-36576-1_27","volume-title":"Foundations of Software Science and Computation Structures","author":"C Sprenger","year":"2003","unstructured":"Sprenger, C., Dam, M.: On the structure of inductive reasoning: circular and tree-shaped proofs in the $$\\mu $$-calculus. In: Gordon, A.D. (ed.) FoSSaCS 2003. LNCS, vol. 2620, pp. 425\u2013440. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36576-1_27"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Zetzsche, S., Silva, A., Sammartino, M.: Guarded Kleene algebra with tests: automata learning. In: Proceedings of the 38th Conference on the Mathematical Foundations of Programming Semantics, MFPS. EPTICS, vol.\u00a01. EpiSciences (2022)","DOI":"10.46298\/entics.10505"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63501-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:04:06Z","timestamp":1719824646000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63501-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031635007","9783031635014"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63501-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"2 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}