Cyclic Proofs, Hypersequents, and Transitive Closure Logic

Anupam Das; Marianna Girlando

doi:10.1007/978-3-031-10769-6_30

Cyclic Proofs, Hypersequents, and Transitive Closure Logic

Anupam Das^*, Marianna Girlando

^*Corresponding author for this work

Computer Science

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

2 Citations (Scopus)

25 Downloads (Pure)

Abstract

We propose a cut-free cyclic system for Transitive Closure Logic (TCL) based on a form of hypersequents, suitable for automated reasoning via proof search. We show that previously proposed sequent systems are cut-free incomplete for basic validities from Kleene Algebra (KA) and Propositional Dynamic Logic (PDL ), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and PDL, thereby inheriting their completeness results. A peculiarity of our system is its richer correctness criterion, exhibiting ‘alternating traces’ and necessitating a more intricate soundness argument than for traditional cyclic proofs.

Original language	English
Title of host publication	Automated Reasoning
Subtitle of host publication	11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022, Proceedings
Editors	Jasmin Blanchette, Laura Kovács, Dirk Pattinson
Publisher	Springer
Pages	509-528
Number of pages	20
Edition	1
ISBN (Electronic)	9783031107696
ISBN (Print)	9783031107689
DOIs	https://doi.org/10.1007/978-3-031-10769-6_30
Publication status	Published - 17 Jul 2022
Event	11th International Joint Conference on Automated Reasoning, IJCAR 2022, part of the Federated Logic Conference, FLoC 2022 - Haifa, Israel Duration: 8 Aug 2022 → 10 Aug 2022

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13385
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Joint Conference on Automated Reasoning, IJCAR 2022, part of the Federated Logic Conference, FLoC 2022
Country/Territory	Israel
City	Haifa
Period	8/08/22 → 10/08/22

Bibliographical note

Funding Information:
This work was supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1.

Publisher Copyright:
© 2022, The Author(s).

Keywords

Cyclic proofs
Hypersequents
Propositional Dynamic Logic
Transitive Closure Logic

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-031-10769-6_30Licence: Creative Commons: Attribution (CC BY)

DasA2022CyclicFinal published version, 692 KBLicence: Creative Commons: Attribution (CC BY)

Structure vs. Invariants in Proofs (StrIP)
Das, A.
Medical Research Council
1/05/20 → 31/07/24
Project: Research Councils

Cite this

Das, A., & Girlando, M. (2022). Cyclic Proofs, Hypersequents, and Transitive Closure Logic. In J. Blanchette, L. Kovács, & D. Pattinson (Eds.), Automated Reasoning: 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022, Proceedings (1 ed., pp. 509-528). (Lecture Notes in Computer Science; Vol. 13385). Springer. https://doi.org/10.1007/978-3-031-10769-6_30

@inproceedings{1e0160efb09542a184a71cdc3bad2ca7,

title = "Cyclic Proofs, Hypersequents, and Transitive Closure Logic",

abstract = "We propose a cut-free cyclic system for Transitive Closure Logic (TCL) based on a form of hypersequents, suitable for automated reasoning via proof search. We show that previously proposed sequent systems are cut-free incomplete for basic validities from Kleene Algebra (KA) and Propositional Dynamic Logic (PDL ), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and PDL, thereby inheriting their completeness results. A peculiarity of our system is its richer correctness criterion, exhibiting {\textquoteleft}alternating traces{\textquoteright} and necessitating a more intricate soundness argument than for traditional cyclic proofs.",

keywords = "Cyclic proofs, Hypersequents, Propositional Dynamic Logic, Transitive Closure Logic",

author = "Anupam Das and Marianna Girlando",

note = "Funding Information: This work was supported by a UKRI Future Leaders Fellowship, {\textquoteleft}Structure vs Invariants in Proofs{\textquoteright}, project reference MR/S035540/1. Publisher Copyright: {\textcopyright} 2022, The Author(s).; 11th International Joint Conference on Automated Reasoning, IJCAR 2022, part of the Federated Logic Conference, FLoC 2022 ; Conference date: 08-08-2022 Through 10-08-2022",

year = "2022",

month = jul,

day = "17",

doi = "10.1007/978-3-031-10769-6_30",

language = "English",

isbn = "9783031107689",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "509--528",

editor = "Jasmin Blanchette and Laura Kov{\'a}cs and Dirk Pattinson",

booktitle = "Automated Reasoning",

edition = "1",

}

Das, A & Girlando, M 2022, Cyclic Proofs, Hypersequents, and Transitive Closure Logic. in J Blanchette, L Kovács & D Pattinson (eds), Automated Reasoning: 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022, Proceedings. 1 edn, Lecture Notes in Computer Science, vol. 13385, Springer, pp. 509-528, 11th International Joint Conference on Automated Reasoning, IJCAR 2022, part of the Federated Logic Conference, FLoC 2022, Haifa, Israel, 8/08/22. https://doi.org/10.1007/978-3-031-10769-6_30

Cyclic Proofs, Hypersequents, and Transitive Closure Logic. / Das, Anupam; Girlando, Marianna.
Automated Reasoning: 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022, Proceedings. ed. / Jasmin Blanchette; Laura Kovács; Dirk Pattinson. 1. ed. Springer, 2022. p. 509-528 (Lecture Notes in Computer Science; Vol. 13385).

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

TY - GEN

T1 - Cyclic Proofs, Hypersequents, and Transitive Closure Logic

AU - Das, Anupam

AU - Girlando, Marianna

PY - 2022/7/17

Y1 - 2022/7/17

N2 - We propose a cut-free cyclic system for Transitive Closure Logic (TCL) based on a form of hypersequents, suitable for automated reasoning via proof search. We show that previously proposed sequent systems are cut-free incomplete for basic validities from Kleene Algebra (KA) and Propositional Dynamic Logic (PDL ), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and PDL, thereby inheriting their completeness results. A peculiarity of our system is its richer correctness criterion, exhibiting ‘alternating traces’ and necessitating a more intricate soundness argument than for traditional cyclic proofs.

AB - We propose a cut-free cyclic system for Transitive Closure Logic (TCL) based on a form of hypersequents, suitable for automated reasoning via proof search. We show that previously proposed sequent systems are cut-free incomplete for basic validities from Kleene Algebra (KA) and Propositional Dynamic Logic (PDL ), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and PDL, thereby inheriting their completeness results. A peculiarity of our system is its richer correctness criterion, exhibiting ‘alternating traces’ and necessitating a more intricate soundness argument than for traditional cyclic proofs.

KW - Cyclic proofs

KW - Hypersequents

KW - Propositional Dynamic Logic

KW - Transitive Closure Logic

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

U2 - 10.1007/978-3-031-10769-6_30

DO - 10.1007/978-3-031-10769-6_30

M3 - Conference contribution

AN - SCOPUS:85135836033

SN - 9783031107689

T3 - Lecture Notes in Computer Science

SP - 509

EP - 528

BT - Automated Reasoning

A2 - Blanchette, Jasmin

A2 - Kovács, Laura

A2 - Pattinson, Dirk

PB - Springer

T2 - 11th International Joint Conference on Automated Reasoning, IJCAR 2022, part of the Federated Logic Conference, FLoC 2022

Y2 - 8 August 2022 through 10 August 2022

ER -