## Paper: Proof Theory for Kleene Algebra (at LICS 2005)

**Chris Hardin**

### Abstract

The universal Horn theory of relational Kleene algebra with tests (RKAT) is of practical interest, particularly for program semantics. We develop an (infinitary) proof system, based on well-founded trees of finite automata, which is sound and complete for this theory. A small modification of this system yields a proof system which is sound and complete for the universal Horn theory of .-continuous Kleene algebras with tests (KAT*). This sheds light on the relationship between RKATand KAT*.

### BibTeX

@InProceedings{Hardin-ProofTheoryforKleen, author = {Chris Hardin}, title = {Proof Theory for Kleene Algebra}, booktitle = {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)}, year = {2005}, month = {June}, pages = {290--299}, location = {Chicago, USA}, publisher = {IEEE Computer Society Press} }