@inproceedings{9c43902b481d443fb1760cc3677b69b9,
title = "Non-wellfounded proof theory for (Kleene+action)(Algebras+lattices)",
abstract = "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.",
keywords = "Kleene algebra, non-wellfounded proofs, proof theory, sequent system",
author = "Anupam Das and Damien Pous",
year = "2018",
month = aug,
day = "1",
doi = "10.4230/LIPIcs.CSL.2018.19",
language = "English",
isbn = "9783959770880",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl",
pages = "19:1 -- 19:18",
editor = "Ghica, {Dan R.} and Achim Jung",
booktitle = "27th EACSL Annual Conference on Computer Science Logic 2018 (CSL 2018)",
address = "Germany",
note = "27th Annual EACSL Conference Computer Science Logic, CSL 2018 ; Conference date: 04-09-2018 Through 07-09-2018",
}