Non-wellfounded proof theory for (Kleene+action)(Algebras+lattices)

Anupam Das, Damien Pous

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)
26 Downloads (Pure)


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.

Original languageEnglish
Title of host publication27th EACSL Annual Conference on Computer Science Logic 2018 (CSL 2018)
EditorsDan R. Ghica, Achim Jung
PublisherSchloss Dagstuhl
Pages19:1 - 19:18
Number of pages18
ISBN (Print)9783959770880
Publication statusPublished - 1 Aug 2018
Event27th Annual EACSL Conference Computer Science Logic, CSL 2018 - Birmingham, United Kingdom
Duration: 4 Sept 20187 Sept 2018

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
ISSN (Print)1868-8969


Conference27th Annual EACSL Conference Computer Science Logic, CSL 2018
Country/TerritoryUnited Kingdom


  • Kleene algebra
  • non-wellfounded proofs
  • proof theory
  • sequent system

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Non-wellfounded proof theory for (Kleene+action)(Algebras+lattices)'. Together they form a unique fingerprint.

Cite this