Terminating sequent calculi for proving and refuting formulas in S4
Camillo Fiorentini · Journal of Logic and Computation · 2012
We present a contraction-free sequent calculus GS4 for the modal logic S4 such that all the rules are decreasing and enjoy the subformula property. We also introduce a refutation calculus RS4 with the same properties of GS4. We provide a proof search algorithm that, given a sequent σ, returns either a proof of σ in GS4 or a refutation of σ in RS4. From a refutation of σ, we can generate an S4-model of σ.