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 σ.
Terminating sequent calculi for proving and refuting formulas in S4 / C. Fiorentini. - In: JOURNAL OF LOGIC AND COMPUTATION. - ISSN 0955-792X. - 25:1(2015 Feb), pp. 179-205. [10.1093/logcom/exs053]
Terminating sequent calculi for proving and refuting formulas in S4
C. Fiorentini
2015
Abstract
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 σ.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
2015_jlc.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
957.74 kB
Formato
Adobe PDF
|
957.74 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
