A cut-free cyclic proof system for kleene algebra

Anupam Das; Damien Pous

doi:10.1007/978-3-319-66902-1_16

A cut-free cyclic proof system for kleene algebra

Anupam Das, Damien Pous^*

^*Corresponding author for this work

Computer Science

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

12 Citations (Scopus)

173 Downloads (Pure)

Abstract

We introduce a sound non-wellfounded proof system whose regular (or ‘cyclic’) proofs are complete for (in)equations between regular expressions. We achieve regularity by using hypersequents rather than usual sequents, with more structure in the succedent, and relying on the discreteness of rational languages to drive proof search. By inspection of the proof search space we extract a PSpace bound for the system, which is optimal for deciding such (in)equations.

Original language	English
Title of host publication	Automated Reasoning with Analytic Tableaux and Related Methods
Subtitle of host publication	26th International Conference, TABLEAUX 2017, Brasilia, Brazil, September 25-28 2017, Proceedings
Editors	Claudia Nalon, Renate A. Schmidt
Publisher	Springer
Pages	261-277
ISBN (Electronic)	9783319669021
ISBN (Print)	9783319669014
DOIs	https://doi.org/10.1007/978-3-319-66902-1_16
Publication status	Published - 30 Aug 2017
Event	26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2017 - Brasilia, Brazil Duration: 25 Sept 2017 → 28 Sept 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10501 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2017
Country/Territory	Brazil
City	Brasilia
Period	25/09/17 → 28/09/17

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-319-66902-1_16Licence: None: All rights reserved

Das_Pous_A_cut-free_cyclic_proof_system_for_Kleene_algebra_TABLEAUX_2017Accepted author manuscript, 405 KBLicence: None: All rights reserved

https://link.springer.com/chapter/10.1007%2F978-3-319-66902-1_16Licence: None: All rights reserved

Cite this

Das, A., & Pous, D. (2017). A cut-free cyclic proof system for kleene algebra. In C. Nalon, & R. A. Schmidt (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasilia, Brazil, September 25-28 2017, Proceedings (pp. 261-277). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10501 LNAI). Springer. https://doi.org/10.1007/978-3-319-66902-1_16

Das, Anupam ; Pous, Damien. / A cut-free cyclic proof system for kleene algebra. Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasilia, Brazil, September 25-28 2017, Proceedings. editor / Claudia Nalon ; Renate A. Schmidt. Springer, 2017. pp. 261-277 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2e9851cf84d74640a2a86b54ae2a0194,

title = "A cut-free cyclic proof system for kleene algebra",

abstract = "We introduce a sound non-wellfounded proof system whose regular (or {\textquoteleft}cyclic{\textquoteright}) proofs are complete for (in)equations between regular expressions. We achieve regularity by using hypersequents rather than usual sequents, with more structure in the succedent, and relying on the discreteness of rational languages to drive proof search. By inspection of the proof search space we extract a PSpace bound for the system, which is optimal for deciding such (in)equations.",

author = "Anupam Das and Damien Pous",

year = "2017",

month = aug,

day = "30",

doi = "10.1007/978-3-319-66902-1_16",

language = "English",

isbn = "9783319669014",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "261--277",

editor = "Claudia Nalon and Schmidt, {Renate A.}",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods",

note = "26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2017 ; Conference date: 25-09-2017 Through 28-09-2017",

}

Das, A & Pous, D 2017, A cut-free cyclic proof system for kleene algebra. in C Nalon & RA Schmidt (eds), Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasilia, Brazil, September 25-28 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10501 LNAI, Springer, pp. 261-277, 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2017, Brasilia, Brazil, 25/09/17. https://doi.org/10.1007/978-3-319-66902-1_16

A cut-free cyclic proof system for kleene algebra. / Das, Anupam; Pous, Damien.
Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasilia, Brazil, September 25-28 2017, Proceedings. ed. / Claudia Nalon; Renate A. Schmidt. Springer, 2017. p. 261-277 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10501 LNAI).

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

TY - GEN

T1 - A cut-free cyclic proof system for kleene algebra

AU - Das, Anupam

AU - Pous, Damien

PY - 2017/8/30

Y1 - 2017/8/30

N2 - We introduce a sound non-wellfounded proof system whose regular (or ‘cyclic’) proofs are complete for (in)equations between regular expressions. We achieve regularity by using hypersequents rather than usual sequents, with more structure in the succedent, and relying on the discreteness of rational languages to drive proof search. By inspection of the proof search space we extract a PSpace bound for the system, which is optimal for deciding such (in)equations.

AB - We introduce a sound non-wellfounded proof system whose regular (or ‘cyclic’) proofs are complete for (in)equations between regular expressions. We achieve regularity by using hypersequents rather than usual sequents, with more structure in the succedent, and relying on the discreteness of rational languages to drive proof search. By inspection of the proof search space we extract a PSpace bound for the system, which is optimal for deciding such (in)equations.

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

U2 - 10.1007/978-3-319-66902-1_16

DO - 10.1007/978-3-319-66902-1_16

M3 - Conference contribution

AN - SCOPUS:85029479143

SN - 9783319669014

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 261

EP - 277

BT - Automated Reasoning with Analytic Tableaux and Related Methods

A2 - Nalon, Claudia

A2 - Schmidt, Renate A.

PB - Springer

T2 - 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2017

Y2 - 25 September 2017 through 28 September 2017

ER -

Das A, Pous D. A cut-free cyclic proof system for kleene algebra. In Nalon C, Schmidt RA, editors, Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasilia, Brazil, September 25-28 2017, Proceedings. Springer. 2017. p. 261-277. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-66902-1_16

A cut-free cyclic proof system for kleene algebra

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this