Automated reasoning in higher-order regular algebra. (English) Zbl 1364.68326

Kahl, Wolfram (ed.) et al., Relational and algebraic methods in computer science. 13th international conference, RAMiCS 2012, Cambridge, UK, September 17–20, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-33313-2/pbk). Lecture Notes in Computer Science 7560, 66-81 (2012).
Summary: We extend a large Isabelle/HOL repository for regular algebras towards higher-order variants based on directed sets and quantales, including reasoning based on general fixpoint properties and Galois connections. In this context we demonstrate that Isabelle’s recent integration of automated theorem proving technology effectively supports higher-order reasoning. We present four case studies that underpin this claim: the calculus of Galois connections and fixpoints, action algebras and Galois connections, solvability conditions for regular equations and fixpoint fusion, and the implementation of formal language quantales.
For the entire collection see [Zbl 1246.68043].


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
06A15 Galois correspondences, closure operators (in relation to ordered sets)
06F07 Quantales
68Q70 Algebraic theory of languages and automata
Full Text: DOI


[1] Aarts, C.J.: Galois connections presented calculationally. Master’s thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology (1992)
[2] Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: Hints in Unification. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 84–98. Springer, Heidelberg (2009) · Zbl 1252.68246
[3] Ballarin, C.: Tutorial to locales and locale interpretation. In: Contribuciones Científicas en honor de Mirian Andrés. Servicio de Publicaciones de la Universidad de La Rioja, Spain (2010)
[4] Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic Proof and Disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 12–27. Springer, Heidelberg (2011) · Zbl 1348.68214
[5] Boffa, M.: Une remarque sur les systèmes complets d’identités rationnelles. Informatique Théorique et Applications 24(4), 419–423 (1990) · Zbl 0701.68059
[6] Boffa, M.: Une condition impliquant toutes les identités rationnelles. Informatique Théorique et Applications 29(6), 515–518 (1995) · Zbl 0881.68071
[7] 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–178. Springer, Heidelberg (2010) · Zbl 1291.68330
[8] Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall (1971) · Zbl 0231.94041
[9] Desharnais, J., Struth, G.: Internal axioms for domain semirings. Science of Computer Programming 76(3), 181–203 (2011) · Zbl 1211.68242
[10] Doornbos, H., Backhouse, R.C., van der Woude, J.: A calculational approach to mathematical induction. Theor. Comput. Sci. 179(1-2), 103–135 (1997) · Zbl 0901.68124
[11] Foster, S., Struth, G.: Automated Analysis of Regular Algebra. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 271–285. Springer, Heidelberg (2012) · Zbl 1358.68254
[12] Foster, S., Struth, G., Weber, T.: Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL – (Invited Tutorial). In: de Swart, H. (ed.) RAMICS 2011. LNCS, vol. 6663, pp. 52–67. Springer, Heidelberg (2011) · Zbl 1329.68230
[13] Gammie, P.: The worker/wrapper transformation. Archive of Formal Proofs, 2009 (2009)
[14] Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging Mathematical Structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327–342. Springer, Heidelberg (2009) · Zbl 1252.68253
[15] 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) · Zbl 05981996
[16] Haftmann, F., Wenzel, M.: Local Theory Specifications in Isabelle/Isar. In: Berardi, S., Damiani, F., de’Liguoro, U. (eds.) TYPES 2008. LNCS, vol. 5497, pp. 153–168. Springer, Heidelberg (2009) · Zbl 1246.68197
[17] Kozen, D.: On Kleene Algebras and Closed Semirings. In: Rovan, B. (ed.) MFCS 1990. LNCS, vol. 452, pp. 26–47. Springer, Heidelberg (1990) · Zbl 0732.03047
[18] Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994) · Zbl 0806.68082
[19] Krauss, A., Nipkow, T.: Proof pearl: Regular expression equivalence and relation algebra. J. Automated Reasoning 49(1), 95–106 (2012) · Zbl 1269.68090
[20] Paulson, L., Nipkow, T., Wenzel, M.: Isabelle (2011), http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html
[21] Pratt, V.R.: Action Logic and Pure Induction. In: van Eijck, J. (ed.) JELIA 1990. LNCS, vol. 478, pp. 97–120. Springer, Heidelberg (1991) · Zbl 0814.03024
[22] Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158–169 (1966) · Zbl 0149.24902
[23] Struth, G.: Left omega algebras and regular equations. J. Logic and Algebraic Programming (in press, 2012) · Zbl 1279.68242
[24] Wu, C., Zhang, X., Urban, C.: A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 341–356. Springer, Heidelberg (2011) · Zbl 1342.68306
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.