Christopher Hardin

Abstract: Kleene algebra arises in many areas of computer science. In particular, Kleene algebra with tests provides an algebraic way of representing and studying programs. When using Kleene algebra for this purpose, one generally wishes to restrict attention to algebras built from binary relations on some set of states, since they capture a common model for computation; such algebras are called relational Kleene algebras.

The equivalence of two programs, which is useful for verifying program correctness or compiler optimizations, can be expressed as an equation in Kleene algebra. The equational theory of relational Kleene algebra is already well understood, and decidable. One often needs to reason about programs under certain hypotheses about the semantics of individual program fragments, however, and this requires the use of Horn formulas.

We show that the Horn theory of relational Kleene algebra is Pi-1-1-complete (highly undecidable). We then exhibit special types of Horn formulas for which the complexity is much lower. We give an infinitary proof system for the Horn theory of relational Kleene algebra that is sound and complete, along with a closely related system that is sound and complete for the Horn theory of *-continuous Kleene algebras. Despite being infinitary, these systems have practical applications; in particular, we give new decidability results that follow from proof-theoretic arguments over the systems