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

Authors: 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}
  }