A Cyclic Proof System for Guarded Kleene Algebra with Tests

Guarded Kleene Algebra with Tests ( \(\texttt{GKAT}\) for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following earlier work by Das and Pous on Kleene Algebra, we study \(\texttt{GKAT}\) from a proof-theoretical perspective. The deterministic nature of \(\texttt{GKAT}\) allows for a non-well-founded sequent system whose set of regular proofs is complete with respect to the guarded language model. This is unlike the situation with Kleene Algebra, where hypersequents are required. Moreover, the decision procedure induced by proof search runs in \(\textsf{NLOGSPACE}\) , whereas that of Kleene Algebra is in \(\textsf{PSPACE}\) .