Paper: Proof Theory for Kleene Algebra (at LICS 2005)
Authors: Chris HardinAbstract
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 Symp. on Logic in Computer Science, {LICS} 2005}, year = 2005, editor = {Prakash Panangaden}, month = {June}, pages = {290--299}, location = {Chicago, USA}, publisher = {IEEE Computer Society Press} }