Home page

The GS4 prover

In the paper 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 σ.

GS4 is a Prolog prototype which implements the proof-search procedure presented in the paper.