Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic
<|reference_start|>Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic: 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.<|reference_end|>
@article{afshari2024cut,
    title={Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic},
    author={Bahareh Afshari, Johannes Kloibhofer},
    journal={arXiv preprint arXiv:2405.01935},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.01935},
    primaryClass={cs.LO math.LO}
}