Programming and automating mathematics in the Tarski-Kleene hierarchy

• 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. 

Ämnesord

NATURVETENSKAP  -- Matematik -- Algebra och logik (hsv//swe)

NATURAL SCIENCES  -- Mathematics -- Algebra and Logic (hsv//eng)

Nyckelord

Formalised mathematics

Interactive theorem proving

Kleene algebra

Relation algebra

Publikations- och innehållstyp

ref (ämneskategori)

art (ämneskategori)