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

FERRARI, MAURO;
2013-01-01

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.
2013
Intuitionistic propositional logic; Sequent calculi; Subformula property; Decision procedures; Counter-models generation
Ferrari, Mauro; Fiorentini, C.; Fiorino, G.
File in questo prodotto:
File Dimensione Formato  
lsint.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 152.24 kB
Formato Adobe PDF
152.24 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11383/1756895
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 19
social impact