{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T18:35:04Z","timestamp":1761935704602,"version":"build-2065373602"},"reference-count":8,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/bf00881949","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:25:12Z","timestamp":1104002712000},"page":"361-373","source":"Crossref","is-referenced-by-count":18,"title":["An improved refutation system for intuitionistic predicate logic"],"prefix":"10.1007","volume":"13","author":[{"given":"Pierangelo","family":"Miglioli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ugo","family":"Moscato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Ornaghi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"CR1","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic,J. Symbolic Logic 57(3) (1992), 795?807.","journal-title":"J. Symbolic Logic"},{"key":"CR2","volume-title":"Intuitionistic Logic, Model Theory and Forcing","author":"M. C. Fitting","year":"1969","unstructured":"Fitting, M. C.:Intuitionistic Logic, Model Theory and Forcing, North-Holland, Amsterdam, 1969."},{"key":"CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2977-2","volume-title":"Semantical Investigations in Heyting's Intuitionistic Logic","author":"D. Gabbay","year":"1981","unstructured":"Gabbay, D.:Semantical Investigations in Heyting's Intuitionistic Logic, Reidel, Dordrecht, 1981."},{"key":"CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-10828-9_72","volume-title":"CAAP '81","author":"P. Miglioli","year":"1981","unstructured":"Miglioli, P., Moscato, U. and Ornaghi, M.: Trees in Kripke models and in an intuitionistic refutation system, in E. Astesiano and C. B\ufffdhm (eds),CAAP '81, Lecture Notes in Computer Science 112, Springer-Verlag, Berlin, 1981, pp. 316?331."},{"key":"CR5","first-page":"646","volume":"32","author":"A. Kolmogorov","year":"1925","unstructured":"Kolmogorov, A.: O principe tertium non datur (On the principle of tertium non datur),Mat. Sb. 32 (1925), 646?667 (in Russian). [English translation in J. van Heijenoort (ed.),From Frege to G\ufffddel, Harvard University Press, Cambridge, 1967, pp. 414?437.]","journal-title":"Mat. Sb."},{"key":"CR6","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1016\/S0049-237X(08)71685-9","volume-title":"Formal Systems and Recursive Functions","author":"S. Kripke","year":"1965","unstructured":"Kripke, S.: Semantical analysis of intuitionistic logic I, in J. N. Crossley and M. A. E. Dummett (eds),Formal Systems and Recursive Functions, North-Holland, Amsterdam, 1965, pp. 92?130."},{"key":"CR7","series-title":"Lecture Notes in Math","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/BFb0066744","volume-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","author":"C. A. Smorinsky","year":"1973","unstructured":"Smorinsky, C. A.: Applications of Kripke models, in A. S. Troelstra (ed.),Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Math. 344, Springer-Verlag, Berlin, 1973, pp. 324?391."},{"key":"CR8","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1016\/S0049-237X(08)71127-3","volume-title":"Handbook of Mathematical Logic","author":"A. S. Troelstra","year":"1977","unstructured":"Troelstra, A. S.: Aspects of constructive mathematics, in J. Barwise (ed.),Handbook of Mathematical Logic, North-Holland, Amsterdam, 1977, pp. 973?1052."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881949.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881949\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881949","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T12:58:12Z","timestamp":1556542692000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881949"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"references-count":8,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994]]}},"alternative-id":["BF00881949"],"URL":"https:\/\/doi.org\/10.1007\/bf00881949","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1994]]}}}