{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T10:45:25Z","timestamp":1648896325696},"reference-count":9,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,9,12]],"date-time":"2012-09-12T00:00:00Z","timestamp":1347408000000},"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":[[2013,2]]},"DOI":"10.1007\/s10817-012-9259-0","type":"journal-article","created":{"date-parts":[[2012,9,12]],"date-time":"2012-09-12T01:01:13Z","timestamp":1347411673000},"page":"135-146","source":"Crossref","is-referenced-by-count":0,"title":["The GOEDEL Program"],"prefix":"10.1007","volume":"50","author":[{"given":"Johan G. F.","family":"Belinfante","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,9,12]]},"reference":[{"key":"9259_CR1","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1023\/A:1006050629424","volume":"22","author":"JGF Belinfante","year":"1999","unstructured":"Belinfante, J.G.F.: Computer proofs in G\u00f6del\u2019s class theory with equational definitions for composite and cross. J. Autom. Reason. 22, 311\u2013339 (1999)","journal-title":"J. Autom. Reason."},{"key":"9259_CR2","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1023\/A:1006010913494","volume":"22","author":"JGF Belinfante","year":"1999","unstructured":"Belinfante, J.G.F.: On computer-assisted proofs in ordinal number theory. J. Autom. Reason. 22, 341\u2013378 (1999)","journal-title":"J. Autom. Reason."},{"key":"9259_CR3","doi-asserted-by":"crossref","first-page":"65","DOI":"10.2307\/2268862","volume":"2","author":"P Bernays","year":"1937","unstructured":"Bernays, P.: A system of axiomatic set theory. J. Symb. Logic 2, 65\u201367 (1937)","journal-title":"J. Symb. Logic"},{"key":"9259_CR4","volume-title":"The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory","author":"K G\u00f6del","year":"1940","unstructured":"G\u00f6del, K.: The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory. Princeton University Press, Princeton (1940)"},{"key":"9259_CR5","doi-asserted-by":"crossref","first-page":"51","DOI":"10.2307\/2308926","volume":"67","author":"JR Isbell","year":"1960","unstructured":"Isbell, J.R.: A definition of ordinal numbers. Am. Math. Mon. 67, 51\u201352 (1960)","journal-title":"Am. Math. Mon."},{"issue":"2","key":"9259_CR6","first-page":"206","volume":"53","author":"J Mycielski","year":"2006","unstructured":"Mycielski, J.: A system of axioms of set theory for the rationalists. Not Am. Math. Soc. 53(2), 206\u2013213 (2006)","journal-title":"Not Am. Math. Soc."},{"key":"9259_CR7","unstructured":"Quaife, A.: Automated development of fundamental mathematical theories. Ph.D. thesis, Univ. of California at Berkeley. Kluwer Academic, Dordrecht (1992)"},{"key":"9259_CR8","doi-asserted-by":"crossref","DOI":"10.4159\/9780674042421","volume-title":"Set Theory and its Logic, revised edn","author":"WV Quine","year":"1963","unstructured":"Quine, W.V.: Set Theory and its Logic, revised edn. The Belknap Press of Harvard University, Cambridge (1963). Footnote on p. 157"},{"key":"9259_CR9","doi-asserted-by":"crossref","first-page":"381","DOI":"10.2307\/2312128","volume":"69","author":"M Sion","year":"1962","unstructured":"Sion, M., Willmott, R.: On a definition of ordinal numbers. Am. Math. Mon. 69, 381\u2013386 (1962)","journal-title":"Am. Math. Mon."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9259-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9259-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9259-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,28]],"date-time":"2022-01-28T18:08:18Z","timestamp":1643393298000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9259-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9,12]]},"references-count":9,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["9259"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9259-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,9,12]]}}}