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)
24 Downloads (Pure)

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.

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
DOIs
Publication statusPublished - 1 Aug 2018
Event27th Annual EACSL Conference Computer Science Logic, CSL 2018 - Birmingham, United Kingdom
Duration: 4 Sep 20187 Sep 2018

Publication series

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

Conference

Conference27th Annual EACSL Conference Computer Science Logic, CSL 2018
Country/TerritoryUnited Kingdom
CityBirmingham
Period4/09/187/09/18

Keywords

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

ASJC Scopus subject areas

  • Software

Fingerprint

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

Cite this