06085009

a

06085009 Armstrong, Alasdair Struth, Georg Automated reasoning in higher-order regular algebra. 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). 2012 Berlin: Springer EN

doi:10.1007/978-3-642-33314-9_5

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.