Title :
Proof theory for Kleene algebra
Author_Institution :
Dept. of Math., Cornell Univ., Ithaca, NY, USA
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 RKAT and KAT*.
Keywords :
Horn clauses; finite automata; relational algebra; theorem proving; trees (mathematics); *-continuous Kleene algebras; KAT*; Kleene algebra proof theory; RKAT; finite automata; infinitary proof system; program semantics; relational Kleene algebra; universal Horn theory; Acoustic testing; Algebra; Algorithm design and analysis; Automata; Computer science; Equations; Heuristic algorithms; Logic; Mathematics; System testing;
Conference_Titel :
Logic in Computer Science, 2005. LICS 2005. Proceedings. 20th Annual IEEE Symposium on
Print_ISBN :
0-7695-2266-1
DOI :
10.1109/LICS.2005.37
