Search

We introduce a single-set axiomatisation of cubical ω -categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical ω -categories, and their variants with connections and inverses, and the corresponding cubical ω -categories. We also report on the formalisation of cubical ω -categories with the Isabelle/HOL proof assistant, which has been instrumental in developing the single-set axiomatisation. [ABSTRACT FROM AUTHOR]

We mechanise a proof of Green's theorem in Isabelle/HOL. We use a novel proof that avoids the ubiquitous line integral cancellation argument. This eliminates the need to formalise orientations and region boundaries explicitly with respect to the outwards-pointing normal vector. Instead we appeal to a homological argument about equivalences between paths. Contributions include mechanised theories of line integrals and partial derivatives, as well as the first mechanisation of Green's theorem. [ABSTRACT FROM AUTHOR]

A recurring proof obligation in modern mathematics, ranging from textbook exercises to deep research problems, is to show that a given function is a morphism in some category: in analysis and topology, for example, we frequently need to prove that functions are continuous, while in group theory we are constantly concerned with homomorphisms. This paper describes a generic procedure that automatically discharges routine instances of this kind of proof obligation in an interactive theorem prover. The proof procedure has been implemented and found very useful in a mathematical case studies carried out using the ProofPower system

We present a principled modular approach to the development of construction and verification tools for imperative programs, in which the control flow and the data flow are cleanly separated. Our simplest verification tool uses Kleene algebra with tests for the control flow of while-programs and their standard relational semantics for the data flow. It is expanded to a basic program construction tool by adding an operation for the specification statement and one single axiom. To include recursive procedures, Kleene algebras with tests are expanded further to quantales with tests. In this more expressive setting, iteration and the specification statement can be defined explicitly and stronger program transformation rules can be derived. Programming our approach in the Isabelle/HOL interactive theorem prover yields simple lightweight mathematical components as well as program construction and verification tools that are correct by construction themselves. Verification condition generation and program construction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. A number of examples shows our tools at work. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

Abstract: Left omega algebras, where one of the usual star induction axioms is absent, are studied in the context of recursive regular equations. Abstract conditions for explicitly defining the omega operation are presented. They are used for developing abstract side conditions on Arden’s rule that are necessary for solving such equations. The definability and solvability results are refined to concrete models, to languages, traces and relations. It turns out, for instance, that the omega operation captures precisely the empty word property in regular languages and wellfoundedness in relational models. The approach also leads to simple new relative completeness results for left omega algebras, and for Salomaa’s axioms for regular expressions. Since automated theorem proving and counterexample search within the theorem proving environment Isabelle/HOL are instrumental for this investigation, it is also an exercise in formalised mathematics. [Copyright &y& Elsevier]