Guarded Kleene Algebra with Tests (GKAT) is a fragment of Kleene Algebra with Tests (KAT) that was recently introduced to reason efficiently about imperative programs. In contrast to KAT, GKAT does not have an algebraic axiomatization, but relies on an analogue of Salomaa's axiomatization of Kleene Algebra. In this paper, we present an algebraic axiomatization and prove two completeness results for a large fragment of GKAT in the form of skip-free programs.

翻译：保护Kleene代数与测试（GKAT）是Kleene代数与测试（KAT）的一个子片段，最近被引入以高效推理命令式程序。与KAT不同，GKAT没有代数公理化，而是依赖于Salomaa对Kleene代数公理化的类比。本文提出了一种代数公理化方法，并证明了GKAT在无跳跃程序这一大片段上的两个完备性结果。