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. © 2012 Springer-Verlag.
CITATION STYLE
Armstrong, A., & Struth, G. (2012). Automated reasoning in higher-order regular algebra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7560 LNCS, pp. 66–81). https://doi.org/10.1007/978-3-642-33314-9_5
Mendeley helps you to discover research relevant for your work.