{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T17:27:59Z","timestamp":1747157279816},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000105"},{"type":"electronic","value":"9783540360780"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36078-6_12","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T02:48:36Z","timestamp":1180666116000},"page":"175-189","source":"Crossref","is-referenced-by-count":1,"title":["On the Complexity of Disjunction and Explicit Definability Properties in Some Intermediate Logics"],"prefix":"10.1007","author":[{"given":"Mauro","family":"Ferrari","sequence":"first","affiliation":[]},{"given":"Camillo","family":"Fiorentini","sequence":"additional","affiliation":[]},{"given":"Guido","family":"Fiorino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"key":"12_CR1","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Logic Based Program Synthesis and Transformation, 10th International Workshop, LOPSTR 2000, Selected Papers","author":"A. Avellone","year":"2001","unstructured":"A. Avellone, M. Ferrari, and C. Fiorentini. A formal framework for synthesis and verification of logic programs. In K.-K. Lau, editor, Logic Based Program Synthesis and Transformation, 10th International Workshop, LOPSTR 2000, Selected Papers, volume 2042 of Lecture Notes in Computer Science, pages 1\u201317. Springer-Verlag, 2001."},{"issue":"3","key":"12_CR2","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0168-0072(99)00002-0","volume":"99","author":"S. Buss","year":"1999","unstructured":"S. Buss and G. Mints. The complexity of the disjunction and existential properties in intuitionistic logic. Annals of Pure and Applied Logic, 99(3):93\u2013104, 1999.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1\u20132","key":"12_CR3","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0168-0072(01)00040-9","volume":"109","author":"S. Buss","year":"2001","unstructured":"S. Buss and P. Pudl\u00e1k. On the computational content of intuitionistic propositional proofs. Annals of Pure and Applied Logic, 109(1\u20132):49\u201364, 2001.","journal-title":"Annals of Pure and Applied Logic"},{"key":"12_CR4","series-title":"PhD thesis","volume-title":"Strongly Constructive Formal Systems","author":"M. Ferrari","year":"1997","unstructured":"M. Ferrari. Strongly Constructive Formal Systems. PhD thesis, Dipartimento di Scienze dell\u2019Informazione, Universit\u00e1 degli Studi di Milano, Italy, 1997. Available at http:\/\/homes.dsi.unimi.it\/~ferram ."},{"key":"12_CR5","unstructured":"M. Ferrari and C. Fiorentini. A proof-theoretical analysis of semiconstructive intermediate theories. Studia Logica, to appear."},{"key":"12_CR6","unstructured":"M. Ferrari, C. Fiorentini, and P. Miglioli. Goal oriented information extraction in uniformly constructive calculi. In Argentinian Workshop on Theoretical Computer Science (WAIT\u201999), pages 51\u201363. Sociedad Argentina de Inform\u00e1tica e Investigaci\u00f3n Operativa, 1999."},{"key":"12_CR7","unstructured":"M. Ferrari, P. Miglioli, and M. Ornaghi. On uniformly constructive and semicon-structive formal systems. Logic Journal of the IGPL, to appear."},{"issue":"6","key":"12_CR8","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1093\/jigpal\/7.6.733","volume":"7","author":"C. Fiorentini","year":"1999","unstructured":"C. Fiorentini and P. Miglioli. A cut-free sequent calculus for the logic of constant domains with a limited amount of duplications. Logic Journal of the IGPL, 7(6):733\u2013753, 1999.","journal-title":"Logic Journal of the IGPL"},{"key":"12_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2977-2","volume-title":"Semantical Investigations in Heyting\u2019s Intuitionistic Logic","author":"D.M. Gabbay","year":"1981","unstructured":"D.M. Gabbay. Semantical Investigations in Heyting\u2019s Intuitionistic Logic. Reidel, Dordrecht, 1981."},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"249","DOI":"10.2307\/2270260","volume":"36","author":"S. G\u00f6rnemann","year":"1971","unstructured":"S. G\u00f6rnemann. A logic stronger than intuitionism. Journal of Symbolic Logic, 36:249\u2013261, 1971.","journal-title":"Journal of Symbolic Logic"},{"key":"12_CR11","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/BF01988049","volume":"3","author":"G. Kreisel","year":"1957","unstructured":"G. Kreisel and H. Putnam. Eine Unableitbarkeitsbeweismethode f\u00fcr den intuition-istischen Aussagenkalk\u00fcl. Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik, 3:74\u201378, 1957.","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"12_CR12","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-1-4613-0897-3_21","volume-title":"Mathematical Logic and its Applications","author":"P. Miglioli","year":"1987","unstructured":"P. Miglioli, U. Moscato, and M. Ornaghi. Constructive theories with abstract data types for program synthesis. In D.G. Skordev, editor, Mathematical Logic and its Applications, pages 293\u2013302. Plenum Press, New York, 1987."},{"issue":"1","key":"12_CR13","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1006\/jsco.1994.1036","volume":"18","author":"P. Miglioli","year":"1994","unstructured":"P. Miglioli, U. Moscato, and M. Ornaghi. Abstract parametric classes and abstract data types defined by classical and constructive logical methods. The Journal of Symbolic Computation, 18(1):41\u201381, 1994.","journal-title":"The Journal of Symbolic Computation"},{"key":"12_CR14","doi-asserted-by":"publisher","first-page":"117","DOI":"10.2977\/prims\/1195193228","volume":"8","author":"H. Ono","year":"1972","unstructured":"H. Ono. Some results on the intermediate logics. Publications of the Research Institute for Mathematical Sciences, Kyoto University, 8:117\u2013130, 1972.","journal-title":"Publications of the Research Institute for Mathematical Sciences, Kyoto University"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"C.A. Smorynski. Applications of Kripke semantics. In A.S. Troelstra, editor, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics, pages 324\u2013391. Springer-Verlag, 1973.","DOI":"10.1007\/BFb0066744"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"A.S. Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer-Verlag, 1973.","DOI":"10.1007\/BFb0066739"},{"key":"12_CR17","unstructured":"A.S. Troelstra and H. Schwichtenberg. Basic Proof Theory, volume 43 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1996."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36078-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:18:02Z","timestamp":1556464682000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36078-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000105","9783540360780"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-36078-6_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}