In this paper we present LSJ, a contraction-free sequent calculus for Intuitionistic propositional logic whose proofs are linearly bounded in the length of the formula to be proved and satisfy the subformula property. We also introduce a sequent calculus RJ for intuitionistic unprovability with the same properties of LSJ. We show that from a refutation of RJ of a sequent σ we can extract a Kripke counter-model for σ . Finally, we provide a procedure that given a sequent σ returns either a proof of σ in LSJ or a refutation in RJ such that the extracted counter-model is of minimal depth.
Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models / M. Ferrari, C. Fiorentini, G. Fiorino. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - 51:2(2013 Aug), pp. 129-149.
Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
C. Fiorentini;
2013
Abstract
In this paper we present LSJ, a contraction-free sequent calculus for Intuitionistic propositional logic whose proofs are linearly bounded in the length of the formula to be proved and satisfy the subformula property. We also introduce a sequent calculus RJ for intuitionistic unprovability with the same properties of LSJ. We show that from a refutation of RJ of a sequent σ we can extract a Kripke counter-model for σ . Finally, we provide a procedure that given a sequent σ returns either a proof of σ in LSJ or a refutation in RJ such that the extracted counter-model is of minimal depth.File | Dimensione | Formato | |
---|---|---|---|
2013_jar.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
1.37 MB
Formato
Adobe PDF
|
1.37 MB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.