A cyclic proof system for Guarded Kleene Algebra with Tests (full version)

Jan Rooduijn, Dexter Kozen, Alexandra Silva

Guarded Kleene Algebra with Tests (GKAT for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following e…