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 consisting of skip-free programs.

翻译：带测试的Kleene代数（KAT）的一个片段——保护型带测试的Kleene代数（GKAT），近期被提出以高效推理命令式程序。与KAT不同，GKAT缺乏代数公理化，而是依赖Salomaa对Kleene代数公理化的类比。本文针对由无跳跃程序构成的GKAT大型片段，提出一种代数公理化方法，并证明两个完备性结果。