Isabelle Repository for Relational and Algebraic Methods


This page contains some theory files for the theorem proving environment Isabelle. Most of the theorems have been obtained by automated reasoning with Isabelle's Sledgehammer tactics or by using SMT solvers.
The files are still experimental and under constant revision and extension. They contain so far more than 800 theorems.
The repository is open for everybody to use and contribute. It will hopefully be replaced by some form of Wiki in the near future. If you want to add theorems to the repository, please either send me a formalised lemma with a Metis/SMT proof that compiles in the respective file, or a handwritten theorem with a detailed manual proof. Please understand that I currently cannot add theorems that require major extensions to the theory files given.

Last changes: 22.01.2015

• Discrete Geometric Model of Concurrent Program Execution
• Taming Multirelations with proofs for the following article
• Concurrent Dynamic Algebra
• Probabilistic Concurrent Kleene Algebra
• Automated Analysis of Regular Algebra
• Left Omega Algebras and Regular Equations
• Aborting, Finite and Infinite Executions (link to Walter Guttmann's web site)
• Locality and the Exchange Law for Concurrent Processes
• Automating Algebraic Methods in Isabelle
• Multiplication
• Dioids
• Kleene algebras
• Omega algebras
• Domain semirings
• Range semirings
• Modal Kleene algebras
• Boolean algebras
• Relation algebras
• Domain semigroups with carrier
• Kleene algebras (another variant for theories below)
• Language Kleene algebras
• Relation Kleene algebras
• Trace Kleene algebras