Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic
| Authors | |
|---|---|
| Publication date | 04-11-2025 |
| Journal | Electronic Proceedings in Theoretical Computer Science |
| Event | 12th Workshop on Fixed Points in Computer Science |
| Volume | Issue number | 435 |
| Pages (from-to) | 21-40 |
| Organisations |
|
| Abstract | We consider modal logic extended with the well-known temporal operator 'eventually' and provide a cut-elimination procedure for a cyclic sequent calculus that captures this fragment. The work showcases an adaptation of the reductive cut-elimination method to cyclic calculi. Notably, the proposed algorithm applies to a cyclic proof and directly outputs a cyclic cut-free proof without appealing to intermediate machinery for regularising the end proof. |
| Document type | Article |
| Note | In: Proceedings Twelfth Workshop on Fixed Points in Computer Science Naples, Italy, 19-20th February 2024. Edited by: Alexis Saurin. |
| Language | English |
| Published at | https://doi.org/10.4204/EPTCS.435.3 |
| Published at | https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?FICS2024.3 |
| Other links | https://cgi.cse.unsw.edu.au/~eptcs/content.cgi?FICS2024 |
| Downloads |
2405.01935v3
(Final published version)
|
| Permalink to this page | |
