Relations and Kleene algebras in computer science

摘要

Relation algebras, Kleene algebras and related algebraic approaches are concerned with the abstraction and compaction of frequently occurring patterns of certain sets of formulas into a form amenable to simple algebraic manipulation, that is, (in)equational reasoning, and hence also to mechanised theorem proving. Among others, they cover the fundamental computer science concepts of choice, sequential composition and (in)finite iteration. These structures have received increasing interest over the last decade, notably through many joint conferences on Relational Methods in Computer Science (RelMiCS) and Applications of Kleene Algebra (AKA).