| Title |
Gentzen-type sequent calculus for modal logic S5 / |
| Authors |
Alonderis, Romas ; Giedra, Haroldas |
| DOI |
10.1093/jigpal/jzaf007 |
| Full Text |
|
| Is Part of |
Logic journal of the IGPL.. Oxford : Oxford University Press. 2025, Early Access, p. [1-12].. ISSN 1367-0751. eISSN 1368-9894 |
| Keywords [eng] |
modal logic S5 ; cut-free sequent calculus ; proof search |
| Abstract [eng] |
We consider a Gentzen-type cut-free sequent calculus GS5 for the modal logic S5 with a restriction on backward applications of modal rule ([]=>). Using Schütte’s method of reduction trees, we prove that the calculus is complete for S5. We also prove that all rules are invertible and the cut rule is admissible in the calculus. We show that any backward proof search terminates, obtaining a decision procedure for S5 using the introduced calculus GS5. |
| Published |
Oxford : Oxford University Press |
| Type |
Journal article |
| Language |
English |
| Publication date |
2025 |
| CC license |
|
