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代数与测试（GKAT）是Kleene代数与测试（KAT）的一个片段，近期被引入用于高效推理命令式程序。与KAT不同，GKAT没有代数公理化，而是依赖于Salomaa对Kleene代数的公理化类比。本文针对由无跳转程序构成的GKAT大型片段，提出了一个代数公理化，并证明了两个完全性结果。