DocumentCode
2023079
Title
Proof theory for Kleene algebra
Author
Hardin, Chris
Author_Institution
Dept. of Math., Cornell Univ., Ithaca, NY, USA
fYear
2005
fDate
26-29 June 2005
Firstpage
290
Lastpage
299
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 2005. LICS 2005. Proceedings. 20th Annual IEEE Symposium on
ISSN
1043-6871
Print_ISBN
0-7695-2266-1
Type
conf
DOI
10.1109/LICS.2005.37
Filename
1509233
Link To Document