A cyclic proof system for Guarded Kleene Algebra with Tests (full version)
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914793812656128 |
|---|---|
| author | Rooduijn, Jan Kozen, Dexter Silva, Alexandra |
| author_facet | Rooduijn, Jan Kozen, Dexter Silva, Alexandra |
| contents | Guarded Kleene Algebra with Tests (GKAT for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following earlier work by Das and Pous on Kleene Algebra, we study GKAT from a proof-theoretical perspective. The deterministic nature of GKAT allows for a non-well-founded sequent system whose set of regular proofs is complete with respect to the guarded language model. This is unlike the situation with Kleene Algebra, where hypersequents are required. Moreover, the decision procedure induced by proof search runs in NLOGSPACE, whereas that of Kleene Algebra is in PSPACE. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_07505 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A cyclic proof system for Guarded Kleene Algebra with Tests (full version) Rooduijn, Jan Kozen, Dexter Silva, Alexandra Logic in Computer Science Formal Languages and Automata Theory Logic Guarded Kleene Algebra with Tests (GKAT for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following earlier work by Das and Pous on Kleene Algebra, we study GKAT from a proof-theoretical perspective. The deterministic nature of GKAT allows for a non-well-founded sequent system whose set of regular proofs is complete with respect to the guarded language model. This is unlike the situation with Kleene Algebra, where hypersequents are required. Moreover, the decision procedure induced by proof search runs in NLOGSPACE, whereas that of Kleene Algebra is in PSPACE. |
| title | A cyclic proof system for Guarded Kleene Algebra with Tests (full version) |
| topic | Logic in Computer Science Formal Languages and Automata Theory Logic |
| url | https://arxiv.org/abs/2405.07505 |