{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T03:52:22Z","timestamp":1752983542194,"version":"3.40.3"},"publisher-location":"Cham","reference-count":54,"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>We investigate the proof theory of regular expressions with fixed points, construed as a notation for (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>\u03c9<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-)context-free grammars. Starting with a hypersequential system for regular expressions due to Das and Pous\u00a0[15], we define its extension by least fixed points and prove the soundness and completeness of its non-wellfounded proofs for the standard language model. From here we apply proof-theoretic techniques to recover an infinitary axiomatisation of the resulting equational theory, complete for inclusions of context-free languages. Finally, we extend our syntax by greatest fixed points, now computing <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>\u03c9<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-context-free languages. We show the soundness and completeness of the corresponding system using a mixture of proof-theoretic and game-theoretic techniques.<\/jats:p>","DOI":"10.1007\/978-3-031-63501-4_13","type":"book-chapter","created":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:02:00Z","timestamp":1719824520000},"page":"237-256","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Proof Theory of\u00a0($$\\omega $$-)Context-Free Languages, via\u00a0Non-wellfounded Proofs"],"prefix":"10.1007","author":[{"given":"Anupam","family":"Das","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abhishek","family":"De","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,2]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Alberucci, L., Kr\u00e4henb\u00fchl, J., Studer, T.: Justifying induction on modal $$\\mu $$-formulae. Logic J. IGPL 22(6), 805\u2013817 (2014). https:\/\/doi.org\/10.1093\/jigpal\/jzu001","DOI":"10.1093\/jigpal\/jzu001"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of the Thirty-Sixth Annual ACM Symposium on Theory of Computing (STOC 2004), pp. 202\u2013211. Association for Computing Machinery, New York (2004). https:\/\/doi.org\/10.1145\/1007352.1007390","DOI":"10.1145\/1007352.1007390"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3) (2009). https:\/\/doi.org\/10.1145\/1516512.1516518","DOI":"10.1145\/1516512.1516518"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114\u2013133 (1981). https:\/\/doi.org\/10.1145\/322234.322243","DOI":"10.1145\/322234.322243"},{"issue":"2","key":"13_CR5","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/S0022-0000(77)80004-4","volume":"15","author":"RS Cohen","year":"1977","unstructured":"Cohen, R.S., Gold, A.Y.: Theory of $$\\omega $$-languagesi, II: characterizations of $$\\omega $$-context-free languages. J. Comput. Syst. Sci. 15(2), 169\u2013208 (1977)","journal-title":"J. Comput. Syst. Sci."},{"key":"13_CR6","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall Mathematics Series. Chapman and Hall (1971)"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Cranch, J., Laurence, M.R., Struth, G.: Completeness results for omega-regular algebras. J. Logic. Algeb. Methods Program. 84(3), 402\u2013425 (2015). https:\/\/doi.org\/10.1016\/j.jlamp.2014.10.002. 13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2012)","DOI":"10.1016\/j.jlamp.2014.10.002"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Curzi, G., Das, A.: Cyclic implicit complexity. In: Baier, C., Fisman, D. (eds.) 37th Annual ACM\/IEEE Symposium on Logic in Computer Science, 2\u20135 August 2022 (LICS 2022), pp. 19:1\u201319:13. ACM, Haifa (2022). https:\/\/doi.org\/10.1145\/3531130.3533340","DOI":"10.1145\/3531130.3533340"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Das, A., De, A.: A proof theory of (omega-)context-free languages, via non-wellfounded proofs (2024). https:\/\/doi.org\/10.48550\/arXiv.2404.16231","DOI":"10.48550\/arXiv.2404.16231"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Das, A., De, A.: A proof theory of right-linear (omega-)grammars via cyclic proofs. arXiv preprint arXiv:2401.13382 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.13382","DOI":"10.48550\/ARXIV.2401.13382"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Das, A., De, A., Saurin, A.: Comparing infinitary systems for linear logic with fixed points. In: Bouyer, P., Srinivasan, S. (eds.) 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0284, pp. 40:1\u201340:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2023). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2023.40","DOI":"10.4230\/LIPIcs.FSTTCS.2023.40"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Das, A., Doumane, A., Pous, D.: Left-handed completeness for kleene algebra, via cyclic proofs. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-22). EPiC Series in Computing, vol.\u00a057, pp. 271\u2013289. EasyChair (2018). https:\/\/doi.org\/10.29007\/hzq3","DOI":"10.29007\/hzq3"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Das, A., Girlando, M.: Cyclic proofs, hypersequents, and transitive closure logic. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning (IJCAR 2022). LNCS, vol. 13385, pp. 509\u2013528. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_30","DOI":"10.1007\/978-3-031-10769-6_30"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Das, A., Girlando, M.: Cyclic hypersequent system for transitive closure logic. J. Autom. Reason. 67(3), 27 (2023). https:\/\/doi.org\/10.1007\/S10817-023-09675-1","DOI":"10.1007\/S10817-023-09675-1"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Das, A., Pous, D.: A cut-free cyclic proof system for Kleene algebra. In: Schmidt, R.A., Nalon, C. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017). LNCS, vol. 10501, pp. 261\u2013277. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66902-1_16","DOI":"10.1007\/978-3-319-66902-1_16"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Das, A., Pous, D.: Non-wellfounded proof theory for (Kleene+Action) (Algebras+Lattices). In: Ghica, D.R., Jung, A. (eds.) 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0119, pp. 19:1\u201319:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2018.19","DOI":"10.4230\/LIPIcs.CSL.2018.19"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"\u00c9sik, Z., Lei, H.: Greibach normal form in algebraically complete semirings. In: Bradfield, J. (ed.) CSL 2002. LNCS, vol. 2471, pp. 135\u2013150. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45793-3_10","DOI":"10.1007\/3-540-45793-3_10"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"\u00c9sik, Z., Lei\u00df, H.: Algebraically complete semirings and greibach normal form. Annal. Pure Appl. Logic 133(1), 173\u2013203 (2005). https:\/\/doi.org\/10.1016\/j.apal.2004.10.008. Festschrift on the occasion of Helmut Schwichtenberg\u2019s 60th birthday","DOI":"10.1016\/j.apal.2004.10.008"},{"issue":"2","key":"13_CR19","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1051\/ita\/2009001","volume":"43","author":"O Finkel","year":"2009","unstructured":"Finkel, O.: Highly undecidable problems for infinite computations. RAIRO - Theor. Inf. Appl. 43(2), 339\u2013364 (2009). https:\/\/doi.org\/10.1051\/ita\/2009001","journal-title":"RAIRO - Theor. Inf. Appl."},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Finkel, O.: The determinacy of context-free games. J. Symbol. Logic 78(4), 1115\u20131134 (2013). http:\/\/www.jstor.org\/stable\/43303700","DOI":"10.2178\/jsl.7804050"},{"issue":"3","key":"13_CR21","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1145\/321127.321132","volume":"9","author":"S Ginsburg","year":"1962","unstructured":"Ginsburg, S., Rice, H.G.: Two families of languages related to algol. J. ACM 9(3), 350\u2013371 (1962)","journal-title":"J. ACM"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Grathwohl, N.B.B., Henglein, F., Kozen, D.: Infinitary axiomatization of the equational theory of context-free languages. Electron. Proc. Theor. Comput. Sci. 126, 44\u201355 (2013). https:\/\/doi.org\/10.4204\/eptcs.126.4","DOI":"10.4204\/eptcs.126.4"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Gruska, J.: A characterization of context-free languages. J. Comput. Syst. Sci. 5(4), 353\u2013364 (1971). https:\/\/doi.org\/10.1016\/S0022-0000(71)80023-5","DOI":"10.1016\/S0022-0000(71)80023-5"},{"issue":"4","key":"13_CR24","doi-asserted-by":"publisher","first-page":"685","DOI":"10.2307\/2273508","volume":"43","author":"L Harrington","year":"1978","unstructured":"Harrington, L.: Analytic determinacy and $$0\\#$$. J. Symb. Log. 43(4), 685\u2013693 (1978). https:\/\/doi.org\/10.2307\/2273508","journal-title":"J. Symb. Log."},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Hazard, E., Kuperberg, D.: Cyclic proofs for transfinite expressions. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), 14\u201319 February 2022, G\u00f6ttingen (Virtual Conference). LIPIcs, vol.\u00a0216, pp. 23:1\u201323:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2022.23","DOI":"10.4230\/LIPICS.CSL.2022.23"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Jipsen, P.: From semirings to residuated kleene lattices. Stud. Logica 76, 291\u2013303 (2004). https:\/\/doi.org\/10.1023\/B:STUD.0000032089.54776.63","DOI":"10.1023\/B:STUD.0000032089.54776.63"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.E., Rajeev Motwani, J.D.U.: Introduction to Automata Theory, Languages, and Computation, 2nd edn. Addison-Wesley (2001)","DOI":"10.1145\/568438.568455"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Kleene, S.C.: Representation of Events in Nerve Nets and Finite Automata, pp. 3\u201342. Princeton University Press, Princeton (1956). https:\/\/doi.org\/10.1515\/9781400882618-002","DOI":"10.1515\/9781400882618-002"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366\u2013390 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1037","DOI":"10.1006\/inco.1994.1037"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theor. Comput. Sci. 27(3), 333\u2013354 (1983). https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6. Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Kozen, D., Silva, A.: Left-handed completeness. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol. 7560, pp. 162\u2013178. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33314-9_11","DOI":"10.1007\/978-3-642-33314-9_11"},{"key":"13_CR32","doi-asserted-by":"publisher","unstructured":"Kozen, D., Silva, A.: Left-handed completeness. Theor. Comput. Sci. 807, 220\u2013233 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2019.10.040. In memory of Maurice Nivat, a founding father of Theoretical Computer Science - Part II","DOI":"10.1016\/j.tcs.2019.10.040"},{"key":"13_CR33","doi-asserted-by":"publisher","unstructured":"Kozen, D., Smith, F.: Kleene algebra with tests: completeness and decidability. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 244\u2013259. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63172-0_43","DOI":"10.1007\/3-540-63172-0_43"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Krishnaswami, N.R., Yallop, J.: A typed, algebraic approach to parsing. In: PLDI (PLDI 2019), pp. 379\u2013393. Association for Computing Machinery, New York (2019). https:\/\/doi.org\/10.1145\/3314221.3314625","DOI":"10.1145\/3314221.3314625"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Krob, D.: A complete system of B-rational identities. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 60\u201373. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032022","DOI":"10.1007\/BFb0032022"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Kupke, C., Marti, J., Venema, Y.: Succinct graph representations of $$\\mu $$-calculus formulas. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0216, pp. 29:1\u201329:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2022.29","DOI":"10.4230\/LIPIcs.CSL.2022.29"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Lange, M.: Local model checking games for fixed point logic with chop. In: Brim, L., Jancar, P., Kret\u00ednsk\u00fd, M., Kucera, A. (eds.) Concurrency Theory. CONCUR 2002. LNCS, vol.\u00a02421, pp. 240\u2013254. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45694-5_17","DOI":"10.1007\/3-540-45694-5_17"},{"key":"13_CR38","doi-asserted-by":"publisher","unstructured":"Lei\u00df, H.: Towards Kleene algebra with recursion. In: B\u00f6rger, E., J\u00e4ger, G., Kleine B\u00fcning, H., Richter, M.M. (eds.) CSL 1991. LNCS, vol. 626, pp. 242\u2013256. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0023771","DOI":"10.1007\/BFb0023771"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Leiss, H.: The matrix ring of a mu-continuous chomsky algebra is mu-continuous. In: Talbot, J.M., Regnier, L. (eds.) 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a062, pp. 6:1\u20136:15. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.6","DOI":"10.4230\/LIPIcs.CSL.2016.6"},{"key":"13_CR40","doi-asserted-by":"publisher","unstructured":"Lei\u00df, H., Hopkins, M.: C-Dioids and $$\\mu $$-continuous chomsky-algebras. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) RAMiCS 2018. LNCS, vol. 11194, pp. 21\u201336. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02149-8_2","DOI":"10.1007\/978-3-030-02149-8_2"},{"key":"13_CR41","doi-asserted-by":"publisher","unstructured":"Li, W., Tanaka, K.: The determinacy strength of pushdown $$\\omega $$-languages. RAIRO-Theor. Inf. Appl. 51(1), 29\u201350 (2017). https:\/\/doi.org\/10.1051\/ita\/2017006","DOI":"10.1051\/ita\/2017006"},{"issue":"3","key":"13_CR42","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1016\/S0019-9958(76)90415-0","volume":"31","author":"M Linna","year":"1976","unstructured":"Linna, M.: On $$\\omega $$-sets associated with context-free languages. Inf. Control 31(3), 272\u2013293 (1976)","journal-title":"Inf. Control"},{"key":"13_CR43","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C., Madhusudan, P., Serre, O.: Visibly pushdown games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 408\u2013420. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30538-5_34","DOI":"10.1007\/978-3-540-30538-5_34"},{"key":"13_CR44","unstructured":"Mansfield, R., Weitkamp, G.: Recursive aspects of descriptive set theory. In: Oxford Logic Guides, Oxford University Press (1985). https:\/\/books.google.co.uk\/books?id=jPzuAAAAMAAJ"},{"issue":"1\u20133","key":"13_CR45","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.tcs.2004.12.029","volume":"337","author":"E Moriya","year":"2005","unstructured":"Moriya, E., Hofbauer, D., Huber, M., Otto, F.: On state-alternating context-free grammars. Theoret. Comput. Sci. 337(1\u20133), 183\u2013216 (2005)","journal-title":"Theoret. Comput. Sci."},{"key":"13_CR46","doi-asserted-by":"crossref","unstructured":"Nivat, M.: Mots infinis engendr\u00e9s par une grammaire alg\u00e9brique. RAIRO - Theor. Inf. Appl. Inf. Th\u00e9or. Appl. 11(4), 311\u2013327 (1977). http:\/\/eudml.org\/doc\/92059","DOI":"10.1051\/ita\/1977110403111"},{"key":"13_CR47","doi-asserted-by":"crossref","unstructured":"Nivat, M.: Sur les ensembles de mots infinis engendr\u00e9s par une grammaire alg\u00e9brique. RAIRO - Theor. Inf. Appl. Inf. Th\u00e9or. Appl. 12(3), 259\u2013278 (1978). http:\/\/eudml.org\/doc\/92080","DOI":"10.1051\/ita\/1978120302591"},{"key":"13_CR48","doi-asserted-by":"publisher","unstructured":"Niwi\u0144ski, D., Walukiewicz, I.: Games for the $$\\mu $$-calculus. Theoret. Comput. Sci. 163(1), 99\u2013116 (1996) https:\/\/doi.org\/10.1016\/0304-3975(95)00136-0","DOI":"10.1016\/0304-3975(95)00136-0"},{"issue":"2","key":"13_CR49","first-page":"295","volume":"78","author":"E Palka","year":"2007","unstructured":"Palka, E.: An infinitary sequent system for the equational theory of *-continuous action lattices. Fund. Inform. 78(2), 295\u2013309 (2007)","journal-title":"Fund. Inform."},{"key":"13_CR50","doi-asserted-by":"publisher","unstructured":"Sacks, G.E.: Higher Recursion Theory. Perspectives in Logic. Cambridge University Press (2017). https:\/\/doi.org\/10.1017\/9781316717301","DOI":"10.1017\/9781316717301"},{"key":"13_CR51","doi-asserted-by":"crossref","unstructured":"Salomaa, A.: Formal Languages. ACM Monograph Series. Academic Press (1973)","DOI":"10.5186\/aasfm.1973.525"},{"key":"13_CR52","doi-asserted-by":"publisher","unstructured":"Sch\u00fctzenberger, M.: On context-free languages and push-down automata. Inf. Control 6(3), 246\u2013264 (1963). https:\/\/doi.org\/10.1016\/S0019-9958(63)90306-1","DOI":"10.1016\/S0019-9958(63)90306-1"},{"issue":"3","key":"13_CR53","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/S11225-008-9133-6","volume":"89","author":"T Studer","year":"2008","unstructured":"Studer, T.: On the proof theory of the modal mu-calculus. Stud. Logica. 89(3), 343\u2013363 (2008). https:\/\/doi.org\/10.1007\/S11225-008-9133-6","journal-title":"Stud. Logica."},{"key":"13_CR54","doi-asserted-by":"publisher","unstructured":"Thiemann, P.: Partial derivatives for context-free languages. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 248\u2013264. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54458-7_15","DOI":"10.1007\/978-3-662-54458-7_15"}],"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_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:03:48Z","timestamp":1719824628000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63501-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031635007","9783031635014"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63501-4_13","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"}}]}}