{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,8,15]],"date-time":"2022-08-15T01:25:06Z","timestamp":1660526706439},"reference-count":8,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1992,3,1]],"date-time":"1992-03-01T00:00:00Z","timestamp":699408000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["BIT"],"published-print":{"date-parts":[[1992,3]]},"DOI":"10.1007\/bf01995108","type":"journal-article","created":{"date-parts":[[2005,8,10]],"date-time":"2005-08-10T14:40:23Z","timestamp":1123684823000},"page":"64-69","source":"Crossref","is-referenced-by-count":3,"title":["Complexity of subclasses of the intuitionistic propositional calculus"],"prefix":"10.1007","volume":"32","author":[{"given":"G.","family":"Mints","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF01995108_CR1","unstructured":"Kleene S. C.,Introduction to Metamathematics. van Nostrand (1952)."},{"key":"BF01995108_CR2","doi-asserted-by":"crossref","unstructured":"Marin-L\u00f6f P., Mints G. (eds),COLOG-88.Lecture Notes in Computer Science, Springer-Verlag v. 417, (1990).","DOI":"10.1007\/3-540-52335-9"},{"key":"BF01995108_CR3","unstructured":"Mints G.,Resolution calculi for the non-classical logics. (Russian). 9 Soviet Symp. in Cybernetics. Moscow, VINITI, (1981)."},{"key":"BF01995108_CR4","doi-asserted-by":"crossref","unstructured":"Mints G.,Gentzen-type systems and resolution rule. Part I. In [2], pp. 198\u2013231.","DOI":"10.1007\/3-540-52335-9_55"},{"key":"BF01995108_CR5","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/0167-6423(83)90016-3","volume":"N2","author":"G. Mints","year":"1982","unstructured":"Mints G., Tyugu E.,Justification of the structural synthesis of programs. Sci. of Comput. Program., (1982), N2, 215\u2013240.","journal-title":"Sci. of Comput. Program."},{"key":"BF01995108_CR6","unstructured":"B. Nordstr\u00f6m, K. Peterson, J. Smith,Programming in Martin-L\u00f6f's Type Theory. An Introduction. Oxford University Press, (1990)."},{"key":"BF01995108_CR7","unstructured":"Orevkov V.,On Glivenko classes of sequents. Proc. Steklov Inst. of Math., (1968), AMS Translations-Series 2, v. 98."},{"key":"BF01995108_CR8","first-page":"45","volume":"46","author":"M. Wajsberg","year":"1938","unstructured":"Wajsberg M.,Untersuchungen \u00fcber den Aussagenkalk\u00fcl von A. Heyting, Wiadomosci Matematyczne, 46, (1938), 45\u2013101.","journal-title":"Wiadomosci Matematyczne"}],"container-title":["BIT"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01995108.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01995108\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01995108","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T20:25:26Z","timestamp":1586377526000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01995108"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,3]]},"references-count":8,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,3]]}},"alternative-id":["BF01995108"],"URL":"https:\/\/doi.org\/10.1007\/bf01995108","relation":{},"ISSN":["0006-3835","1572-9125"],"issn-type":[{"value":"0006-3835","type":"print"},{"value":"1572-9125","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,3]]}}}