In this paper we study the complexity of disjunction property for Intuitionistic Logic, the modal logics S3, S4.1, Grzegorczyk Logic, Godel-Lob Logic and the intuitionistic counterpart of the modal logic K. For S4 we even prove the feasible interpolation theorem and we provide a lower bound for the length of proofs. The techniques we use do not require to prove structural properties of the calculi in hand, such as the Cut-elimination Theorem or the Normalization Theorem. This is a key-point of our approach, since it allows us to treat logics for which only Hilbert-style characterizations are known.

On the complexity of the disjunction property in intuitionistic and modal logics / M. Ferrari, C. Fiorentini, G. Fiorino. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 6:3(2005), pp. 519-538.

On the complexity of the disjunction property in intuitionistic and modal logics

C. Fiorentini;
2005

Abstract

In this paper we study the complexity of disjunction property for Intuitionistic Logic, the modal logics S3, S4.1, Grzegorczyk Logic, Godel-Lob Logic and the intuitionistic counterpart of the modal logic K. For S4 we even prove the feasible interpolation theorem and we provide a lower bound for the length of proofs. The techniques we use do not require to prove structural properties of the calculi in hand, such as the Cut-elimination Theorem or the Normalization Theorem. This is a key-point of our approach, since it allows us to treat logics for which only Hilbert-style characterizations are known.
Feasible interpolation; Intuitionistic logic; Modal logic; Proof-length
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
Article (author)
File in questo prodotto:
File Dimensione Formato  
2005_tocl.pdf

accesso aperto

Tipologia: Publisher's version/PDF
Dimensione 169.09 kB
Formato Adobe PDF
169.09 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

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: http://hdl.handle.net/2434/4800
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact