On the Fine-Structure of Regular Algebra

Article English OPEN
Foster, Simon David; Struth, Georg;
  • Subject:
    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 sys... View more
  • References (31)
    31 references, page 1 of 4

    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)

  • Metrics
Share - Bookmark