Home page
The GS4 prover
In the paper
-
C. Fiorentini.
Terminating sequent calculi for proving and
refuting formulas in S4.
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 σ.
GS4 is a Prolog prototype which implements the proof-search procedure
presented in the paper.
-
The prover (Prolog prototype):
.tar
-
Examples of proofs in the calculus
GS4:
.tar
-
Examples of refutations in the calculus
RS4:
.tar