{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:58:27Z","timestamp":1759147107548},"reference-count":17,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2005,7]]},"abstract":"<jats:p>In this article we study the complexity of disjunction property for intuitionistic logic, the modal logics<jats:bold>S4<\/jats:bold>,<jats:bold>S4.1<\/jats:bold>, Grzegorczyk logic, G\u00f6del-L\u00f6b logic, and the intuitionistic counterpart of the modal logic<jats:bold>K<\/jats:bold>. For<jats:bold>S4<\/jats:bold>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.<\/jats:p>","DOI":"10.1145\/1071596.1071598","type":"journal-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T08:30:55Z","timestamp":1123057855000},"page":"519-538","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["On the complexity of the disjunction property in intuitionistic and modal logics"],"prefix":"10.1145","volume":"6","author":[{"given":"Mauro","family":"Ferrari","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano, Milan, Italy"}]},{"given":"Camillo","family":"Fiorentini","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano, Milan, Italy"}]},{"given":"Guido","family":"Fiorino","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano-Bicocca, Milan, Italy"}]}],"member":"320","published-online":{"date-parts":[[2005,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/BF01053021","article-title":"A uniform tableau method for intuitionistic modal logics I&ast;","volume":"53","author":"Amati G.","year":"1994","journal-title":"Studia Logica"},{"key":"e_1_2_1_2_1","volume-title":"10th International Workshop, LOPSTR 2000, Selected Papers, K.-K. Lau, Ed. Lecture Notes in Computer Science","volume":"2042","author":"Avellone A."},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","first-page":"935","DOI":"10.2307\/2274147","article-title":"On modal systems having arithmetical interpretations","volume":"49","author":"Avron A.","year":"1984","journal-title":"J. Symbol. Logic"},{"key":"e_1_2_1_4_1","volume-title":"Computational Logic (Marktoberdorf","author":"Buss S.","year":"1997"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/S0168-0072(99)00002-0","article-title":"The complexity of the disjunction and existential properties in intuitionistic logic","volume":"99","author":"Buss S.","year":"1999","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0168-0072(01)00040-9","article-title":"On the computational content of intuitionistic propositional proofs","volume":"109","author":"Buss S.","year":"2001","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Chagrov A. and Zakharyaschev M. 1997. Modal Logic. Oxford University Press Oxford U.K.]] Chagrov A. and Zakharyaschev M. 1997. Modal Logic. Oxford University Press Oxford U.K.]]","DOI":"10.1093\/oso\/9780198537793.001.0001"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1023\/A:1022985222183","article-title":"A proof-theoretical analysis of semiconstructive intermediate theories","volume":"73","author":"Ferrari M.","year":"2003","journal-title":"Studia Logica"},{"key":"e_1_2_1_9_1","volume-title":"LPAR 2002: Logic for Programming Artificial Intelligence and Reasoning. Lecture Notes in Artificial Intelligence","volume":"2514","author":"Ferrari M."},{"key":"e_1_2_1_10_1","volume-title":"Argentinian Workshop on Theoretical Computer Science (WAIT'99)","author":"Ferrari M."},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/jigpal\/11.1.1","article-title":"On uniformly constructive and semiconstructive formal systems","volume":"11","author":"Ferrari M.","year":"2003","journal-title":"Logic J. IGPL"},{"key":"e_1_2_1_12_1","first-page":"179","article-title":"Axiomatizations for some intuitionistic modal logics","volume":"42","author":"Fischer Servi G.","year":"1984","journal-title":"Rend. Sem. Mat. Univers. Polit. Torino"},{"key":"e_1_2_1_13_1","volume-title":"Bounded arithmetic, propositional logic, and complexity theory. Encyclopedia of Mathematics and its Applications","author":"Kraj\u00ed\u010dek J."},{"key":"e_1_2_1_14_1","volume-title":"Natural Deduction. Almquist and Winksell","author":"Prawitz D."},{"key":"e_1_2_1_15_1","volume-title":"Sets and Proofs (Leeds","author":"Pudl\u00e1k P.","year":"1997"},{"key":"e_1_2_1_16_1","volume-title":"Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science","volume":"43","author":"Troelstra A."},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1007\/BF00249262","article-title":"The modal logic of provability: cut-elimination","volume":"12","author":"Valentini S.","year":"1983","journal-title":"J. Philos. Logic"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1071596.1071598","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,28]],"date-time":"2024-01-28T12:38:03Z","timestamp":1706445483000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1071596.1071598"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,7]]},"references-count":17,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,7]]}},"alternative-id":["10.1145\/1071596.1071598"],"URL":"https:\/\/doi.org\/10.1145\/1071596.1071598","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,7]]},"assertion":[{"value":"2005-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}