Left-handed completeness for Kleene algebra, via cyclic proofs

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

Authors

Colleges, School and Institutes

External organisations

  • University of Copenhagen
  • Université de Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP

Abstract

We give a new proof that the axioms of left-handed Kleene algebra are complete with respect to language containments. This proof is significantly simpler than both the proof of Boffa (which relies on Krob’s completeness result), and the more recent proof of Kozen and Silva. Our proof builds on a recent non-wellfounded sequent calculus which makes it possible to explicitly compute the invariants required for left-handed Kleene algebra

Details

Original languageEnglish
Title of host publicationLPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
EditorsGilles Barthe, Geoff Sutcliffe, Margus Veanes
Publication statusPublished - 23 Oct 2018
Event22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Awassa, Ethiopia
Duration: 16 Nov 201821 Nov 2018

Publication series

NameEPiC Series in Computing
PublisherEasyChair
Volume57
ISSN (Electronic)2398-7340

Conference

Conference22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
CountryEthiopia
CityAwassa
Period16/11/1821/11/18

Keywords

  • automata, axiomatisation, cyclic proofs, induction, Kleene algebra, regular languages