Sciweavers

Share
LICS
2005
IEEE

Proof Theory for Kleene Algebra

11 years 7 months ago
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∗ .
Chris Hardin
Added 25 Jun 2010
Updated 25 Jun 2010
Type Conference
Year 2005
Where LICS
Authors Chris Hardin
Comments (0)
books