Proof Theory for Kleene Algebra

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 RKAT and KAT∗ .

• Type: Conference
• Year: 2005
• Where: LICS
• Authors: Chris Hardin
• Keywords: Computer Science, Kleene Algebras, LICS 2005, Relational Kleene Algebra, Universal Horn Theory