{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:32:49Z","timestamp":1784845969818,"version":"3.55.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030171261","type":"print"},{"value":"9783030171278","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T00:00:00Z","timestamp":1554422400000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We study the Horn theories of Kleene algebras and star continuous Kleene algebras, from the complexity point of view. While their equational theories coincide and are <jats:sc>PSpace<\/jats:sc>-complete, their Horn theories differ and are undecidable. We characterise the Horn theory of star continuous Kleene algebras in terms of downward closed languages and we show that when restricting the shape of allowed hypotheses, the problems lie in various levels of the arithmetical or analytical hierarchy. We also answer a question posed by Cohen about hypotheses of the form <jats:inline-formula>\n              <jats:tex-math>$$1=S$$<\/jats:tex-math>\n            <\/jats:inline-formula> where <jats:italic>S<\/jats:italic> is a sum of letters: we show that it is decidable.<\/jats:p>","DOI":"10.1007\/978-3-030-17127-8_12","type":"book-chapter","created":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T11:11:46Z","timestamp":1554462706000},"page":"207-223","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Kleene Algebra with Hypotheses"],"prefix":"10.1007","author":[{"given":"Amina","family":"Doumane","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Denis","family":"Kuperberg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Damien","family":"Pous","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9cilia","family":"Pradic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,4,5]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Anderson, C.J., et al.: NetKAT: semantic foundations for networks. In: Proceedings of the POPL, pp. 113\u2013126. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535862","DOI":"10.1145\/2535838.2535862"},{"key":"12_CR2","unstructured":"Angus, A., Kozen, D.: Kleene algebra with tests and program schematology. Technical report TR2001-1844, CS Dpt., Cornell University, July 2001. http:\/\/hdl.handle.net\/1813\/5831"},{"key":"12_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). http:\/\/archive.numdam.org\/article\/ITA19902444190.pdf","journal-title":"Informatique Th\u00e9orique et Applications"},{"key":"12_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":"12_CR5","unstructured":"Cohen, E.: Hypotheses in Kleene algebra. Technical report, Bellcore, Morristown, N.J. (1994). http:\/\/www.researchgate.net\/publication\/2648968_Hypotheses_in_Kleene_Algebra"},{"key":"12_CR6","volume-title":"Regular Algebra and Finite Machines","author":"JH Conway","year":"1971","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Das, A., Doumane, A., Pous, D.: Left-handed completeness for Kleene algebra, via cyclic proofs. In: Proceedings of the LPAR. EPiC Series in Computing, vol. 57, pp. 271\u2013289. EasyChair (2018). https:\/\/doi.org\/10.29007\/hzq3","DOI":"10.29007\/hzq3"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Doumane, A., Kuperberg, D., Pous, D., Pradic, C.: Kleene algebra with hypotheses. Full version of this extended abstract (2019). https:\/\/hal.archives-ouvertes.fr\/hal-02021315","DOI":"10.1007\/978-3-030-17127-8_12"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-642-04081-8_27","volume-title":"CONCUR 2009 - Concurrency Theory","author":"CART Hoare","year":"2009","unstructured":"Hoare, C.A.R.T., M\u00f6ller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 399\u2013414. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04081-8_27"},{"key":"12_CR10","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). http:\/\/www.rand.org\/pubs\/research_memoranda\/2008\/RM704.pdf","DOI":"10.1515\/9781400882618-002"},{"issue":"2","key":"12_CR11","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. Inform. Comput. 110(2), 366\u2013390 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1037","journal-title":"Inform. Comput."},{"issue":"1","key":"12_CR12","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). https:\/\/doi.org\/10.1145\/343369.343378","journal-title":"ACM Trans. Comput. Log."},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1006\/inco.2001.2960","volume":"179","author":"D Kozen","year":"2002","unstructured":"Kozen, D.: On the complexity of reasoning in Kleene algebra. Inform. Comput. 179, 152\u2013162 (2002). https:\/\/doi.org\/10.1006\/inco.2001.2960","journal-title":"Inform. Comput."},{"key":"12_CR14","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":"12_CR15","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"},{"issue":"1","key":"12_CR16","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/s10817-011-9223-4","volume":"49","author":"A Krauss","year":"2012","unstructured":"Krauss, A., Nipkow, T.: Proof pearl: regular expression equivalence and relation algebra. JAR 49(1), 95\u2013106 (2012). https:\/\/doi.org\/10.1007\/s10817-011-9223-4","journal-title":"JAR"},{"issue":"2","key":"12_CR17","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/0304-3975(91)90395-I","volume":"89","author":"D Krob","year":"1991","unstructured":"Krob, D.: Complete systems of B-rational identities. TCS 89(2), 207\u2013343 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90395-I","journal-title":"TCS"},{"key":"12_CR18","unstructured":"Mamouras, K.: Extensions of Kleene algebra for program verification. Ph.D. thesis, Cornell University, Ithaca, NY (2015). https:\/\/ecommons.cornell.edu\/handle\/1813\/40960"},{"key":"12_CR19","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"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17127-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,5]],"date-time":"2025-09-05T17:07:57Z","timestamp":1757092077000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-17127-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171261","9783030171278"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17127-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}