Programming and Automating Mathematics in the Tarski-Kleene Hierarchy

Alasdair Armstrong, Georg Struth, and Tjark Weber. Journal of Logical and Algebraic Methods in Programming, 83(2):87-102, March 2014.

Abstract

We present examples from a reference implementation of variants of Kleene algebras and Tarski's relation algebras in the theorem proving environment Isabelle/HOL. For Kleene algebras we show how models can be programmed, including sets of traces and paths, languages, binary relations, max-plus and min-plus algebras, matrices, formal power series. For relation algebras we discuss primarily proof automation in a comprehensive library and present an advanced formalisation example.

Download

• PDF (320 kB)

BibTeX

@article{armstrong14programming,
  author    = {Alasdair Armstrong and Georg Struth and Tjark Weber},
  title     = {Programming and Automating Mathematics in the {Tarski}-{Kleene} Hierarchy},
  journal   = {Journal of Logical and Algebraic Methods in Programming},
  volume    = {83},
  number    = {2},
  pages     = {87--102},
  publisher = {Elsevier},
  month     = mar,
  year      = 2014,
  url       = {http://dx.doi.org/10.1016/j.jlap.2014.02.001},
}