{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:05:12Z","timestamp":1759147512747,"version":"3.41.0"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1998,8,1]],"date-time":"1998-08-01T00:00:00Z","timestamp":901929600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,8,1]],"date-time":"1998-08-01T00:00:00Z","timestamp":901929600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1998,8]]},"DOI":"10.1023\/a:1005888712422","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:56:21Z","timestamp":1040514981000},"page":"69-97","source":"Crossref","is-referenced-by-count":3,"title":["Nonconstructive Computational Mathematics"],"prefix":"10.1007","volume":"21","author":[{"given":"Kenneth","family":"Kunen","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"144607_CR1","unstructured":"Aho, A. V., Hopcroft, J. E. and Ullman, J. D.: Data Structures and Algorithms, Addison-Wesley, 1983."},{"key":"144607_CR2","doi-asserted-by":"crossref","unstructured":"Beeson, M. L.: Foundations of Constructive Mathematics, Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-68952-9"},{"key":"144607_CR3","doi-asserted-by":"crossref","unstructured":"Boyer, B. S., Goldschlag, D., Kaufmann, M. and Moore, J S.: Functional Instantiation in First Order Logic, in Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, V. Lifschitz (ed.), Academic Press, 1991, pp. 7\u201326.","DOI":"10.1016\/B978-0-12-450010-5.50007-4"},{"key":"144607_CR4","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF00244392","volume":"4","author":"R. S. Boyer","year":"1988","unstructured":"Boyer, R. S. and Moore, J S.: The addition of bounded quantification and partial functions to a computational logic and its theorem prover, J. Automated Reasoning\n4 (1988), 117\u2013172.","journal-title":"J. Automated Reasoning"},{"key":"144607_CR5","unstructured":"Boyer, R. S. and Moore, J S.: A Computational Logic Handbook, Academic Press, 1988."},{"key":"144607_CR6","unstructured":"Brock, B. C. and Hunt, W. A.: An Overview of the Formal Specification and Verification of the FM9001 Microprocessor, preprint, currently available on WWW at http:\/\/www.cli.com\/hardware\/fm9001.html."},{"key":"144607_CR7","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/BF01565428","volume":"112","author":"G. Gentzen","year":"1936","unstructured":"Gentzen, G.: Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen\n112 (1936), 493\u2013565.","journal-title":"Mathematische Annalen"},{"key":"144607_CR8","first-page":"34","volume":"4","author":"K. G\u00f6del","year":"1933","unstructured":"G\u00f6del, K.: Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines Mathematischen Kolloquiums\n4 (1933), 34\u201338, reprinted in Feferman, Dawson, Kleene, Moore, Solovay, and van Heijenoort, Kurt G\u00f6del Collected Works Vol. 1, Oxford University Press, 1986.","journal-title":"Ergebnisse eines Mathematischen Kolloquiums"},{"key":"144607_CR9","unstructured":"Goodstein, R. L.: Recursive Number Theory, North-Holland 1964."},{"key":"144607_CR10","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/BF00245295","volume":"9","author":"M. Kaufmann","year":"1992","unstructured":"Kaufmann, M.: An extension of the Boyer-Moore theorem prover to support first-order quantification, J. Automated Reasoning\n9 (1992), 355\u2013372.","journal-title":"J. Automated Reasoning"},{"key":"144607_CR11","doi-asserted-by":"crossref","first-page":"267","DOI":"10.2307\/2006985","volume":"113","author":"J. Ketonen","year":"1981","unstructured":"Ketonen, J. and Solovay, S.: Rapidly growing Ramsey functions, Annals of Math.\n113 (1981), 267\u2013314.","journal-title":"Annals of Math."},{"key":"144607_CR12","unstructured":"Kleene, S. C.: Introduction to Metamathematics, Van Nostrand, 1952."},{"key":"144607_CR13","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/BF00881917","volume":"15","author":"K. Kunen","year":"1995","unstructured":"Kunen, K.: A Ramsey theorem in Boyer-Moore logic, J. Automated Reasoning\n15 (1995), 217\u2013235.","journal-title":"J. Automated Reasoning"},{"key":"144607_CR14","doi-asserted-by":"crossref","unstructured":"Paris, J. and Harrington, L.: A mathematical incompleteness in Peano arithmetic, in Handbook of Mathematical Logic, J. Barwise (ed.), North-Holland, 1978, pp. 1133\u20131142.","DOI":"10.1016\/S0049-237X(08)71130-3"},{"key":"144607_CR15","unstructured":"Parsons, C.: On a Number-theoretic choice scheme and its relation to induction, in Intuitionism and Proof Theory, Kino, Myhill, and Vessley (eds), North-Holland, pp. 459\u2013473. See also JSL\n37 (1972), 466\u2013482."},{"key":"144607_CR16","first-page":"33","volume":"28","author":"W. Sieg","year":"1985","unstructured":"Sieg, W.: Fragments of arithmetic, APAL\n28 (1985), 33\u201371.","journal-title":"APAL"},{"key":"144607_CR17","unstructured":"Troelstra, A. S.: Constructivism in Mathematics Vol. 1, North-Holland, 1988."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005888712422.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005888712422\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005888712422.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:25:34Z","timestamp":1749122734000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005888712422"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,8]]},"references-count":17,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1998,8]]}},"alternative-id":["144607"],"URL":"https:\/\/doi.org\/10.1023\/a:1005888712422","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,8]]}}}