Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Foster, Simon David; Struth, Georg (2014)
Languages: English
Types: Article

Classified by OpenAIRE into

arxiv: Computer Science::Logic in Computer Science
Regular algebra is the algebra of regular expressions as induced by regular language identity. We use Isabelle/HOL for a detailed systematic study of the regular algebra axioms given by Boffa, Conway, Kozen and Salomaa. We investigate the relationships between these systems, formalise a soundness proof for the smallest class (Salomaa’s) and obtain completeness for the largest one (Boffa’s) relative to a deep result by Krob. As a case study in formalised mathematics, our investigations also shed some light on the power of theorem proving technology for reasoning with algebras and their models, including proof automation and counterexample generation.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • 1. Armstrong, A., Struth, G., Weber, T.: Kleene algebra. Archive of Formal Proofs 2013 (2013)
    • 2. Benzmu¨ller, C., Sultana, N.: Leo-II Version 1.5. In: J.C. Blanchette, J. Urban (eds.) PxTP 2013, EPiC Series, vol. 14, pp. 2-10. EasyChair (2013)
    • 3. Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: C. Tinelli, V. Sofronie-Stokkermans (eds.) FroCos 2011, LNAI, vol. 6989, pp. 12-27. Springer (2011)
    • 4. Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: M. Kaufmann, L.C. Paulson (eds.) Interactive Theorem Proving, LNCS, vol. 6172, pp. 131-146. Springer (2010). DOI 10.1007/978-3-642-14052-5 11
    • 5. Bloom, S.L., E´ sik, Z.: Equational axioms for regular sets. Mathematical Structures in Computer Science 3(1), 1-24 (1993)
    • 6. Boffa, M.: Une remarque sur les syste`mes complets d'identite´s rationnelles. Informatique the´orique et applications 24(4), 419-423 (1990)
    • 7. Boffa, M.: Une condition impliquant toutes les identite´s rationnelles. Informatique the´orique et applications 29(6), 515-518 (1995)
    • 8. Braibant, T., Pous, D.: An efficient Coq tactic for deciding Kleene algebras. In: M. Kaufmann, L. Paulson (eds.) ITP 2010, LNCS, vol. 6172, pp. 163-178. Springer (2010)
    • 9. Bulwahn, L.: The new Quickcheck for Isabelle. In: C. Hawblitzel, D. Miller (eds.) Certified Programs and Proofs, LNCS, vol. 7679, pp. 92-108. Springer (2012)
    • 10. Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall (1971)
    • 11. Eilenberg, S.: Automata, Languages and Machines. Academic Press (1976)
    • 12. E´sik, Z.: Group axioms for iteration. Information and Computation 148(2), 131-180 (1999)
    • 13. Foster, S., Struth, G.: Regular algebras. Archive of Formal Proofs 2014 (2014)
    • 14. Ginzburg, A.: Algebraic Theory of Automata. Academic Press (1968)
    • 15. Gordon, M.J.C., Reynolds, J., Hunt, W.A., Kaufmann, M.: An integration of HOL and ACL2. In: FMCAD 2006, pp. 153-160. IEEE Computer Society (2006)
    • 16. Guttmann, W.: Algebras for iteration and infinite computations. Acta Informatica 49(5), 343-359 (2012)
    • 17. H o¨fner, P., Struth, G.: Algebraic notions of nontermination: Omega and divergence in idempotent semirings. J. Logic and Algebraic Programming 79(8), 794-811 (2010)
    • 18. Huffman, B., Kuncar, O.: Lifting and transfer: A modular design for quotients in Isabelle/HOL. In: G. Gonthier, M. Norrish (eds.) CPP 2013, LNCS, vol. 8307, pp. 131-146. Springer International Publishing (2013)
    • 19. Iancu, M., Rabe, F.: Formalizing foundations of mathematics. Mathematical Structures in Computer Science 21, 883-911 (2011)
    • 20. Kleene, S.C.: Representation of events in nerve nets and finite automata. In: C.E. Shannon, J. McCarthy (eds.) Automata Studies, chap. 1956, pp. 3-41. Princeton University Press (1956)
    • 21. Kozen, D.: On Kleene algebras and closed semirings. In: B. Rovan (ed.) MFCS'90, LNCS, vol. 452, pp. 26-47. Springer (1990)
    • 22. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110(2), 366-390 (1994)
    • 23. Kozen, D., Silva, A.: Left-handed completeness. In: W. Kahl, T.G. Griffin (eds.) RAMiCS 2012, LNCS, vol. 7560, pp. 162-178. Springer (2012)
    • 24. Krob, D.: Complete systems of B-rational identities. Theoretical Computer Science 89, 207-343 (1991)
    • 25. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)
    • 26. Nipkow, T., Traytel, D.: Unified decision procedures for regular expression equivalence. In: G. Klein, R. Gamboa (eds.) ITP 2014, LNCS, vol. 8558, pp. 450-466. Springer (2014)
    • 27. Pratt, V.: Action logic and pure induction. Tech. Rep. STAN-CS-90-1343, Department of Computer Science, Stanford University (1990)
    • 28. Redko, V.N.: On the determining totality of an algebra of regular events. Ukrain. Math. Z. 16, 120-126 (1964). (in Russian)
    • 29. Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158-169 (1966)
    • 30. Wu, C., Zhang, X., Urban, C.: A formalisation of the myhill-nerode theorem based on regular expressions. J. Autom. Reasoning 52(4), 451-480 (2014)
    • lift-definition plus-reg-lan :: ′a reg-lan ⇒ ′a reg-lan ⇒ ′a reg-lan is plus by (metis (hide-lams, no-types) image-iff lang.simps(4) rangeI) lift-definition times-reg-lan :: ′a reg-lan ⇒ ′a reg-lan ⇒ ′a reg-lan is times by (metis (hide-lams, no-types) image-iff lang.simps(5) rangeI)
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article