A cyclic proof system for Guarded Kleene Algebra with Tests (full version)
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要