Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices)
Anupam Das, Damien Pous · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2018
We prove cut-elimination for a sequent-style proof system which is sound and complete for the equational theory of Kleene algebra, and where proofs are (potentially) non-wellfounded infinite trees. We extend these results to systems with meets and residuals, capturing `star-continuous' action lattices in a similar way. We recover the equational theory of all action lattices by restricting to regular proofs (with cut) - those proofs that are unfoldings of finite graphs.