A cut-free cyclic proof system for kleene algebra

We introduce a sound non-wellfounded proof system whose regular (or ‘cyclic’) proofs are complete for (in)equations between regular expressions. We achieve regularity by using hypersequents rather than usual sequents, with more structure in the succedent, and relying on the discreteness of rational languages to drive proof search. By inspection of the proof search space we extract a PSpace bound for the system, which is optimal for deciding such (in)equations.