A cyclic proof system for Guarded Kleene Algebra with Tests (full version)
CoRR(2024)
Abstract
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.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined