@article{10.1145/1071596.1071598,
    Abstract = {In this article we study the complexity of disjunction property for intuitionistic logic, the modal logics S4, S4.1, Grzegorczyk logic, G\"{o}del-L\"{o}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.},
    Address = {New York, NY, USA},
    Author = {Ferrari, Mauro and Fiorentini, Camillo and Fiorino, Guido},
    File = {On the Complexity of the Disjunction Property in Intuitionistic and Modal Logics - 2005\_tocl - a - v.pdf},
    ISSN = {1529-3785},
    Journal = {ACM Trans. Comput. Logic},
    Keywords = {proof-length, feasible interpolation, modal logic, Intuitionistic logic},
    Month = {July},
    Number = {3},
    Pages = {519--538},
    Publisher = {Association for Computing Machinery},
    Title = {On the Complexity of the Disjunction Property in Intuitionistic and Modal Logics},
    URL = {https://doi.org/10.1145/1071596.1071598},
    Volume = {6},
    Year = {2005},
    bdsk-url-1 = {https://doi.org/10.1145/1071596.1071598},
    date-added = {2020-09-14 10:00:32 +0200},
    date-modified = {2020-09-14 10:00:32 +0200},
    issue_date = {July 2005},
    numpages = {20},
    doi = {10.1145/1071596.1071598}
}

@article{10.1145/1071596.1071598, Abstract = {In this article we study the complexity of disjunction property for intuitionistic logic, the modal logics S4, S4.1, Grzegorczyk logic, G\"{o}del-L\"{o}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.}, Address = {New York, NY, USA}, Author = {Ferrari, Mauro and Fiorentini, Camillo and Fiorino, Guido}, File = {On the Complexity of the Disjunction Property in Intuitionistic and Modal Logics - 2005_tocl - a - v.pdf}, ISSN = {1529-3785}, Journal = {ACM Trans. Comput. Logic}, Keywords = {proof-length, feasible interpolation, modal logic, Intuitionistic logic}, Month = {July}, Number = {3}, Pages = {519--538}, Publisher = {Association for Computing Machinery}, Title = {On the Complexity of the Disjunction Property in Intuitionistic and Modal Logics}, URL = {https://doi.org/10.1145/1071596.1071598}, Volume = {6}, Year = {2005}, bdsk-url-1 = {https://doi.org/10.1145/1071596.1071598}, date-added = {2020-09-14 10:00:32 +0200}, date-modified = {2020-09-14 10:00:32 +0200}, issue_date = {July 2005}, numpages = {20}, doi = {10.1145/1071596.1071598} }