In this article we study the complexity of disjunction property for intuitionistic logic, the modal logics S4, S4.1, Grzegorczyk logic, Gödel-Löb 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 proving 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

Ferrari, M., Fiorentini, C., Fiorino, G. (2005). On the complexity of the disjunction property in intuitionistic and modal logics. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 6(3), 519-538 [10.1145/1071596.1071598].

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

Fiorino, G
2005

Abstract

In this article we study the complexity of disjunction property for intuitionistic logic, the modal logics S4, S4.1, Grzegorczyk logic, Gödel-Löb 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 proving 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
Articolo in rivista - Articolo scientifico
intuitionistic logic, complexity of disjunction property, feasible interpolation
English
2005
6
3
519
538
none
Ferrari, M., Fiorentini, C., Fiorino, G. (2005). On the complexity of the disjunction property in intuitionistic and modal logics. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 6(3), 519-538 [10.1145/1071596.1071598].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/10281/997
Citazioni
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
Social impact