On the Fine-Structure of Regular Algebra

Article English OPEN
Foster, Simon David ; Struth, Georg (2014)
  • Subject:
    acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES | TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
    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.
  • 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
    0
    views in OpenAIRE
    0
    views in local repository
    31
    downloads in local repository

    The information is available from the following content providers:

    From Number Of Views Number Of Downloads
    White Rose Research Online - IRUS-UK 0 31
Share - Bookmark