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

TL;DR

This paper develops a cut-elimination procedure for cyclic proofs in a temporal logic with the 'eventually' operator, demonstrating an effective method for simplifying cyclic proofs directly.

Contribution

It introduces a novel cut-elimination algorithm tailored for cyclic sequent calculi in temporal logic, avoiding intermediate regularisation steps.

Findings

The algorithm successfully eliminates cuts in cyclic proofs.

It directly produces cut-free cyclic proofs without additional machinery.

The method adapts reductive cut-elimination to cyclic proof systems.

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.