Left-handed completeness for Kleene algebra, via cyclic proofs

Anupam Das; Amina Doumane; Damien Pous

doi:10.29007/hzq3

Left-handed completeness for Kleene algebra, via cyclic proofs

Anupam Das, Amina Doumane, Damien Pous

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

10 Citations (Scopus)

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

Original language	English
Title of host publication	LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Editors	Gilles Barthe, Geoff Sutcliffe, Margus Veanes
Publisher	EasyChair Publications
Pages	271-289
Number of pages	19
DOIs	https://doi.org/10.29007/hzq3
Publication status	Published - 23 Oct 2018
Event	22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Awassa, Ethiopia Duration: 16 Nov 2018 → 21 Nov 2018

Publication series

Name	EPiC Series in Computing
Publisher	EasyChair
Volume	57
ISSN (Electronic)	2398-7340

Conference

Conference	22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Country/Territory	Ethiopia
City	Awassa
Period	16/11/18 → 21/11/18

Bibliographical note

Funding Information:
∗This work has been funded by the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, grant agreement No. 678157, and MiLC, grant agreement No. 753431).

Publisher Copyright:
© 2018, EasyChair. All rights reserved.

Keywords

automata
axiomatisation
cyclic proofs
induction
Kleene algebra
regular languages

ASJC Scopus subject areas

Computer Science(all)

Access to Document

10.29007/hzq3Licence: None: All rights reserved

https://easychair.org/publications/paper/SDqfLicence: None: All rights reserved

Cite this

@inproceedings{b1ea30c499e247a5acc7527d2b0437f7,

title = "Left-handed completeness for Kleene algebra, via cyclic proofs",

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{\textquoteright}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",

keywords = "automata, axiomatisation, cyclic proofs, induction, Kleene algebra, regular languages",

author = "Anupam Das and Amina Doumane and Damien Pous",

note = "Funding Information: ∗This work has been funded by the European Research Council (ERC) under the European Union{\textquoteright}s Horizon 2020 programme (CoVeCe, grant agreement No. 678157, and MiLC, grant agreement No. 753431). Publisher Copyright: {\textcopyright} 2018, EasyChair. All rights reserved.; 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning ; Conference date: 16-11-2018 Through 21-11-2018",

year = "2018",

month = oct,

day = "23",

doi = "10.29007/hzq3",

language = "English",

series = "EPiC Series in Computing",

publisher = "EasyChair Publications",

pages = "271--289",

editor = "Gilles Barthe and Geoff Sutcliffe and Margus Veanes",

booktitle = "LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning",

}

Das, A, Doumane, A & Pous, D 2018, Left-handed completeness for Kleene algebra, via cyclic proofs. in G Barthe, G Sutcliffe & M Veanes (eds), LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 57, EasyChair Publications, pp. 271-289, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16/11/18. https://doi.org/10.29007/hzq3

Left-handed completeness for Kleene algebra, via cyclic proofs. / Das, Anupam; Doumane, Amina; Pous, Damien.
LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. ed. / Gilles Barthe; Geoff Sutcliffe; Margus Veanes. EasyChair Publications, 2018. p. 271-289 (EPiC Series in Computing; Vol. 57).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Left-handed completeness for Kleene algebra, via cyclic proofs

AU - Das, Anupam

AU - Doumane, Amina

AU - Pous, Damien

N1 - Funding Information: ∗This work has been funded by the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, grant agreement No. 678157, and MiLC, grant agreement No. 753431). Publisher Copyright: © 2018, EasyChair. All rights reserved.

PY - 2018/10/23

Y1 - 2018/10/23

N2 - 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

AB - 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

KW - automata

KW - axiomatisation

KW - cyclic proofs

KW - induction

KW - Kleene algebra

KW - regular languages

UR - http://www.scopus.com/inward/record.url?scp=85064896028&partnerID=8YFLogxK

U2 - 10.29007/hzq3

DO - 10.29007/hzq3

M3 - Conference contribution

T3 - EPiC Series in Computing

SP - 271

EP - 289

BT - LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning

A2 - Barthe, Gilles

A2 - Sutcliffe, Geoff

A2 - Veanes, Margus

PB - EasyChair Publications

T2 - 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning

Y2 - 16 November 2018 through 21 November 2018

ER -

Left-handed completeness for Kleene algebra, via cyclic proofs

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this