{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:25:26Z","timestamp":1743024326580,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030887001"},{"type":"electronic","value":"9783030887018"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-88701-8_23","type":"book-chapter","created":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T23:06:25Z","timestamp":1634857585000},"page":"378-395","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["On Tools for Completeness of Kleene Algebra with Hypotheses"],"prefix":"10.1007","author":[{"given":"Damien","family":"Pous","sequence":"first","affiliation":[]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[]},{"given":"Jana","family":"Wagemaker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,22]]},"reference":[{"key":"23_CR1","unstructured":"Angus, A., Kozen, D.: Kleene algebra with tests and program schematology. Technical Report TR2001-1844, CS Dpt., Cornell University, July 2001"},{"key":"23_CR2","unstructured":"Birkhoff, G., Bartee, T.C.: Modern Applied Algebra. McGraw-Hill (1970)"},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1051\/ita\/1990240404191","volume":"24","author":"M Boffa","year":"1990","unstructured":"Boffa, M.: Une remarque sur les syst\u00e8mes complets d\u2019identit\u00e9s rationnelles. Informatique Th\u00e9orique et Applications 24, 419\u2013428 (1990)","journal-title":"Informatique Th\u00e9orique et Applications"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-14052-5_13","volume-title":"Interactive Theorem Proving","author":"T Braibant","year":"2010","unstructured":"Braibant, T., Pous, D.: An efficient coq tactic for deciding kleene algebras. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 163\u2013178. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_13"},{"key":"23_CR5","unstructured":"Brunet, P.: A note on commutative Kleene algebra. CoRR, abs\/1910.14381 (2019)"},{"key":"23_CR6","unstructured":"Brunet, P., Pous, D., Struth, G.: On decidability of concurrent Kleene algebra. In: CONCUR, vol. 85 of LIPIcs, pp. 24:1\u201324:16. Schloss Dagstuhl (2017)"},{"key":"23_CR7","unstructured":"Cohen, E.: Hypotheses in Kleene algebra. Tech. rep., Bellcore, N.J. (1994)"},{"key":"23_CR8","unstructured":"Conway, J.: Regular Algebra and Finite Machines. Chapman and Hall mathematics series. Dover Publications, Incorporated (2012)"},{"key":"23_CR9","unstructured":"Davey, B., Priestley, H.: Introduction to Lattices and Order. Cambridge University Press (1990)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-030-17127-8_12","volume-title":"Foundations of Software Science and Computation Structures","author":"A Doumane","year":"2019","unstructured":"Doumane, A., Kuperberg, D., Pous, D., Pradic, P.: Kleene algebra with hypotheses. In: Boja\u0144czyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 207\u2013223. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17127-8_12"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Hardin, C.: Modularizing elimination of r = 0 in Kleene algebra. In: LMCS, vol. 1, no. 3 (2005)","DOI":"10.2168\/LMCS-1(3:4)2005"},{"key":"23_CR12","unstructured":"Hardin, C., Kozen, D.: On the elimination of hypotheses in Kleene algebra with tests. Technical report TR2002-1879, CS Dpt., Cornell University, October 2002"},{"issue":"6","key":"23_CR13","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1016\/j.jlap.2011.04.005","volume":"80","author":"T Hoare","year":"2011","unstructured":"Hoare, T., M\u00f6ller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Logic Algebraic Program. 80(6), 266\u2013296 (2011)","journal-title":"J. Logic Algebraic Program."},{"key":"23_CR14","unstructured":"Kapp\u00e9, T.: Concurrent Kleene Algebra: Completeness and Decidability. PhD thesis, UCL, London (2020)"},{"key":"23_CR15","unstructured":"Kapp\u00e9, T., Brunet, P., Rot, J., Silva, A., Wagemaker, J., Zanasi, F.: Kleene algebra with observations. In: CONCUR, pp. 41:1\u201341:16 (2019)"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-030-45231-5_20","volume-title":"Foundations of Software Science and Computation Structures","author":"T Kapp\u00e9","year":"2020","unstructured":"Kapp\u00e9, T., Brunet, P., Silva, A., Wagemaker, J., Zanasi, F.: Concurrent Kleene algebra with observations: from hypotheses to completeness. In: FoSSaCS 2020. LNCS, vol. 12077, pp. 381\u2013400. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45231-5_20"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Automata Studies, pp. 3\u201341. Princeton University Press (1956)","DOI":"10.1515\/9781400882618-002"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Kozen, D.: A completeness theorem for Kleene Algebras and the algebra of regular events. In: LICS, pp. 214\u2013225. IEEE Computer Society (1991)","DOI":"10.1109\/LICS.1991.151646"},{"issue":"2","key":"23_CR19","first-page":"366","volume":"110","author":"D Kozen","year":"1994","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. I&C 110(2), 366\u2013390 (1994)","journal-title":"I&C"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Kozen, D.: On action algebras. In: Logic and Information Flow, pp. 78\u201388. MIT Press (1994)","DOI":"10.7551\/mitpress\/4286.003.0007"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-61042-1_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kozen","year":"1996","unstructured":"Kozen, D.: Kleene algebra with tests and commutativity conditions. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 14\u201333. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61042-1_35"},{"issue":"3","key":"23_CR22","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. Trans. Program. Lang. Syst. 19(3), 427\u2013443 (1997)","journal-title":"Trans. Program. Lang. Syst."},{"issue":"1","key":"23_CR23","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D Kozen","year":"2000","unstructured":"Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log. 1(1), 60\u201376 (2000)","journal-title":"ACM Trans. Comput. Log."},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Kozen, D.: On the complexity of reasoning in Kleene algebra, p. 179. I&C (2002)","DOI":"10.1006\/inco.2001.2960"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-662-43951-7_24","volume-title":"Automata, Languages, and Programming","author":"D Kozen","year":"2014","unstructured":"Kozen, D., Mamouras, K.: Kleene algebra with equations. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 280\u2013292. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43951-7_24"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/3-540-44957-4_38","volume-title":"Computational Logic \u2014 CL 2000","author":"D Kozen","year":"2000","unstructured":"Kozen, D., Patron, M.-C.: Certification of compiler optimizations using Kleene algebra with tests. In: Lloyd, J., et al. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 568\u2013582. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44957-4_38"},{"key":"23_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/3-540-63172-0_43","volume-title":"Computer Science Logic","author":"D Kozen","year":"1997","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"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Krob, D.: Complete systems of B-rational identities. T.C.S. 89(2), 207\u2013343 (1991)","DOI":"10.1016\/0304-3975(91)90395-I"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Meyer, A., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential space. In: SWAT, pp. 125\u2013129. IEEE (1972)","DOI":"10.1109\/SWAT.1972.29"},{"key":"23_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-642-39634-2_15","volume-title":"Interactive Theorem Proving","author":"D Pous","year":"2013","unstructured":"Pous, D.: Kleene algebra with tests and coq tools for while programs. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 180\u2013196. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_15"},{"key":"23_CR31","doi-asserted-by":"crossref","unstructured":"Pous, D., Rot, J., Wagemaker, J.: On tools for completeness of Kleene algebra with hypotheses. Extended version of the present paper, with proofs, available on HAL at https:\/\/hal.archives-ouvertes.fr\/hal-03269462\/ (2021)","DOI":"10.1007\/978-3-030-88701-8_23"},{"key":"23_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BFb0018436","volume-title":"Logics in AI","author":"V Pratt","year":"1991","unstructured":"Pratt, V.: Action logic and pure induction. In: van Eijck, J. (ed.) JELIA 1990. LNCS, vol. 478, pp. 97\u2013120. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0018436"},{"key":"23_CR33","first-page":"185","volume":"16","author":"V Redko","year":"1964","unstructured":"Redko, V.: On the algebra of commutative events. Ukrain. Mat 16, 185\u2013195 (1964)","journal-title":"Ukrain. Mat"}],"container-title":["Lecture Notes in Computer Science","Relational and Algebraic Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88701-8_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T13:12:35Z","timestamp":1725973955000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88701-8_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030887001","9783030887018"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88701-8_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"22 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RAMiCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Relational and Algebraic Methods in Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marseille","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ramics2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ramics19.lis-lab.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}