Authors

B. Afshari
J. Kloibhofer

Date (dd-mm-yyyy)

2025-11-04

Title

Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic

Journal

Electronic Proceedings in Theoretical Computer Science

Volume

435

Publication Year

2025-11-04

Pages

21-40

Document type

Article

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.

URL

go to publisher's site

Note

Proceedings Twelfth Workshop on Fixed Points in Computer Science : Naples, Italy, 19-20th February 2024.

Permalink

https://hdl.handle.net/11245.1/ec6d34b6-80b8-4071-8767-54ead4b05cb4