2026-07-23T20:59:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9686 2024-03-06T10:44:49Z ddc:004 open_access

Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices) Das, Anupam Pous, Damien Kleene algebra proof theory sequent system non-wellfounded proofs 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Anupam Das and Damien Pous 2018 Is Part Of LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2018.19 urn:nbn:de:0030-drops-96869 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.19 eng https://creativecommons.org/licenses/by/3.0/legalcode