Abstract
Regular algebras axiomatise the equational theory of regular expressions. We use Isabelle/HOL’s automated theorem provers and counterexample generators to study the regular algebras of Boffa, Conway, Kozen and Salomaa, formalise their soundness and completeness (relative to a deep result by Krob) and engineer their hierarchy. Proofs range from fully automatic axiomatic and inductive calculations to integrated higher-order reasoning with numbers, sets and monoid submorphisms. In combination with Isabelle’s simplifiers and structuring mechanisms, automated deduction provides powerful support to the working mathematician beyond first-order reasoning.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Ballarin, C.: Tutorial to locales and locale interpretation. In: Lambán, L., Romero, A., Rubio, J. (eds.) Contribuciones Científicas en honor de Mirian Andrés. Servicio de Publicationes de la Universidad de La Rioja (2010)
Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic Proof and Disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCos 2011. LNCS (LNAI), vol. 6989, pp. 12–27. Springer, Heidelberg (2011)
Boffa, M.: Une remarque sur les systèmes complets d’identités rationnelles. Informatique théorique et Applications 24(4), 419–423 (1990)
Boffa, M.: Une condition impliquant toutes les identités rationnelles. Informatique théorique et Applications 29(6), 515–518 (1995)
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–178. Springer, Heidelberg (2010)
Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall (1971)
Guttmann, W., Struth, G., Weber, T.: Automating Algebraic Methods in Isabelle. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 617–632. Springer, Heidelberg (2011)
Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994)
Krauss, A., Nipkow, T.: Proof pearl: Regular expression equivalence and relation algebra. J. Autom. Reasoning (2011)
Krob, D.: Complete systems of \(\mathcal{B}\)-rational identities. Theoretical Computer Science 89, 207–343 (1991)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158–169 (1966)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Foster, S., Struth, G. (2012). Automated Analysis of Regular Algebra. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-31365-3_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31364-6
Online ISBN: 978-3-642-31365-3
eBook Packages: Computer ScienceComputer Science (R0)