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 earlier work by Das and Pous on Kleene Algebra, we study GKAT from a proof-theoretical perspective. The deterministic nature of 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 NLOGSPACE, whereas that of Kleene Algebra is in PSPACE.

翻译：带守卫的Kleene代数与测试（简称GKAT）是带测试的Kleene代数的一个高效子片段，适用于对简单的命令式while程序进行推理。借鉴Das和Pous在Kleene代数方面的早期工作，我们从证明论角度研究GKAT。GKAT的确定性本质允许构建一个非良基的矢列系统，其正则证明集相对于守卫语言模型是完备的。这与Kleene代数的情况不同——后者需要超矢列系统。此外，由证明搜索导出的判定过程运行于NLOGSPACE复杂度，而Kleene代数的判定过程则属于PSPACE。