{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:15:53Z","timestamp":1759637753686,"version":"3.40.5"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,12,3]],"date-time":"2014-12-03T00:00:00Z","timestamp":1417564800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10817-014-9318-9","type":"journal-article","created":{"date-parts":[[2014,12,2]],"date-time":"2014-12-02T12:49:34Z","timestamp":1417524574000},"page":"165-197","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["On the Fine-Structure of Regular Algebra"],"prefix":"10.1007","volume":"54","author":[{"given":"Simon","family":"Foster","sequence":"first","affiliation":[]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,12,3]]},"reference":[{"key":"9318_CR1","unstructured":"Armstrong, A., Struth, G., Weber, T.: Kleene algebra. Archive of Formal Proofs 2013 (2013)"},{"key":"9318_CR2","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Sultana, N.: Leo-II Version 1.5. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013, EPiC Series, vol. 14, pp. 2\u201310. EasyChair (2013)","DOI":"10.29007\/lbxw"},{"key":"9318_CR3","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCos 2011, LNAI, vol. 6989, pp. 12\u201327. Springer (2011)","DOI":"10.1007\/978-3-642-24364-6_2"},{"key":"9318_CR4","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, LNCS, vol. 6172, pp. 131\u2013146. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_11"},{"issue":"1","key":"9318_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0960129500000104","volume":"3","author":"SL Bloom","year":"1993","unstructured":"Bloom, S.L., \u00c9sik, Z.: Equational axioms for regular sets. Math. Struct. Comput. Sci. 3(1), 1\u201324 (1993)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"4","key":"9318_CR6","doi-asserted-by":"crossref","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. Inf. th\u00e9orique et Appl. 24(4), 419\u2013423 (1990)","journal-title":"Inf. th\u00e9orique et Appl."},{"issue":"6","key":"9318_CR7","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1051\/ita\/1995290605151","volume":"29","author":"M Boffa","year":"1995","unstructured":"Boffa, M.: Une condition impliquant toutes les identit\u00e9s rationnelles. Inf. th\u00e9orique et Appl. 29(6), 515\u2013518 (1995)","journal-title":"Inf. th\u00e9orique et Appl."},{"key":"9318_CR8","doi-asserted-by":"crossref","unstructured":"Braibant, T., Pous, D.: An efficient Coq tactic for deciding Kleene algebras. In: Kaufmann, M., Paulson, L. (eds.) ITP 2010, LNCS, vol. 6172, pp. 163\u2013178. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_13"},{"key":"9318_CR9","doi-asserted-by":"crossref","unstructured":"Bulwahn, L.: The new Quickcheck for Isabelle. In: Hawblitzel, C., Miller, D. (eds.) Certified Programs and Proofs, LNCS, vol. 7679, pp. 92\u2013108. Springer (2012)","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"9318_CR10","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall (1971)"},{"key":"9318_CR11","unstructured":"Eilenberg, S.: Automata, Languages and Machines. Academic Press (1976)"},{"issue":"2","key":"9318_CR12","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1006\/inco.1998.2746","volume":"148","author":"Z \u00c9sik","year":"1999","unstructured":"\u00c9sik, Z.: Group axioms for iteration. Inf. Comput. 148(2), 131\u2013180 (1999)","journal-title":"Inf. Comput."},{"key":"9318_CR13","unstructured":"Foster, S., Struth, G.: Regular algebras. Archive of Formal Proofs 2014 (2014)"},{"key":"9318_CR14","doi-asserted-by":"crossref","unstructured":"Ginzburg, A.: Algebraic Theory of Automata. Academic Press (1968)","DOI":"10.1016\/B978-1-4832-0013-2.50009-6"},{"key":"9318_CR15","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C., Reynolds, J., Hunt, W.A., Kaufmann, M.: An integration of HOL and ACL2, FMCAD 2006, pp 153\u2013160. IEEE Computer Society (2006)","DOI":"10.1109\/FMCAD.2006.6"},{"issue":"8","key":"9318_CR16","doi-asserted-by":"crossref","first-page":"794","DOI":"10.1016\/j.jlap.2010.07.016","volume":"79","author":"P H\u00f6fner","year":"2010","unstructured":"H\u00f6fner, P., Struth, G.: Algebraic notions of nontermination: Omega and divergence in idempotent semirings. J. Logic Algebraic Program. 79(8), 794\u2013811 (2010)","journal-title":"J. Logic Algebraic Program."},{"key":"9318_CR17","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kuncar, O.: Lifting and transfer: A modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013, LNCS, vol. 8307, pp. 131\u2013146. Springer International Publishing (2013)","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"9318_CR18","doi-asserted-by":"crossref","first-page":"883","DOI":"10.1017\/S0960129511000144","volume":"21","author":"M Iancu","year":"2011","unstructured":"Iancu, M., Rabe, F.: Formalizing foundations of mathematics. Math. Struct. Comput. Sci. 21, 883\u2013911 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9318_CR19","doi-asserted-by":"crossref","unstructured":"Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies, chapter 1956, pp 3\u201341. Princeton University Press (1956)","DOI":"10.1515\/9781400882618-002"},{"key":"9318_CR20","doi-asserted-by":"crossref","unstructured":"Kozen, D.: On Kleene algebras and closed semirings. In: Rovan, B. (ed.) MFCS\u201990, LNCS, vol. 452, pp 26\u201347. Springer (1990)","DOI":"10.1007\/BFb0029594"},{"issue":"2","key":"9318_CR21","doi-asserted-by":"crossref","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."},{"key":"9318_CR22","doi-asserted-by":"crossref","unstructured":"Kozen, D., Silva, A.: Left-handed completeness. In: Kahl, W., Griffin, T.G. (eds.) RAMiCS 2012, LNCS, vol. 7560, pp 162\u2013178. Springer (2012)","DOI":"10.1007\/978-3-642-33314-9_11"},{"key":"9318_CR23","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/0304-3975(91)90395-I","volume":"89","author":"D Krob","year":"1991","unstructured":"Krob, D.: Complete systems of \u212c $\\mathcal {B}$ -rational identities. Theor. Comput. Sci. 89, 207\u2013343 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"9318_CR24","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9318_CR25","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Traytel, D.: Unified decision procedures for regular expression equivalence. In: Klein, G., Gamboa, R. (eds.) ITP 2014, LNCS, vol. 8558, pp 450\u2013466. Springer (2014)","DOI":"10.1007\/978-3-319-08970-6_29"},{"key":"9318_CR26","unstructured":"Pratt, V.: Action logic and pure induction. Technical Report STAN-CS-90-1343, Department of Computer Science. Stanford University (1990)"},{"key":"9318_CR27","first-page":"120","volume":"16","author":"VN Redko","year":"1964","unstructured":"Redko, V.N.: On the determining totality of an algebra of regular events. Ukrain. Math. Z 16, 120\u2013126 (1964). (in Russian)","journal-title":"Ukrain. Math. Z"},{"issue":"1","key":"9318_CR28","doi-asserted-by":"crossref","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"},{"issue":"4","key":"9318_CR29","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/s10817-013-9297-2","volume":"52","author":"C Wu","year":"2014","unstructured":"Wu, C., Zhang, X., Urban, C.: A formalisation of the myhill-nerode theorem based on regular expressions. J. Autom. Reason. 52(4), 451\u2013480 (2014)","journal-title":"J. Autom. Reason."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9318-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-014-9318-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9318-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T22:22:30Z","timestamp":1747174950000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-014-9318-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,3]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["9318"],"URL":"https:\/\/doi.org\/10.1007\/s10817-014-9318-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2014,12,3]]}}}