{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,17]],"date-time":"2025-04-17T14:09:09Z","timestamp":1744898949981},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,11,1]],"date-time":"2014-11-01T00:00:00Z","timestamp":1414800000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Minds &amp; Machines"],"published-print":{"date-parts":[[2014,11]]},"DOI":"10.1007\/s11023-014-9349-3","type":"journal-article","created":{"date-parts":[[2014,11,4]],"date-time":"2014-11-04T20:05:01Z","timestamp":1415131501000},"page":"439-476","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["The Comprehensibility Theorem and the Foundations of Artificial Intelligence"],"prefix":"10.1007","volume":"24","author":[{"given":"Arthur","family":"Charlesworth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,11,6]]},"reference":[{"key":"9349_CR1","volume-title":"Modern compiler implementation in Java","author":"AW Appel","year":"1998","unstructured":"Appel, A. W. (1998). Modern compiler implementation in Java. New York: Cambridge University Press."},{"key":"9349_CR2","doi-asserted-by":"crossref","first-page":"711","DOI":"10.1090\/S0002-9904-1976-14122-5","volume":"82","author":"K Appel","year":"1976","unstructured":"Appel, K., & Haken, W. (1976). Every planar map is four colorable. Bulletin of the American Mathematical Society, 82, 711\u2013712.","journal-title":"Bulletin of the American Mathematical Society"},{"key":"9349_CR3","unstructured":"Burgess, J. P. (1992). Proofs about proofs: A defense of classical logic. Part I: The aims of classical logic. In Proof, logic and formalization (pp. 8\u201323). London: Routledge."},{"key":"9349_CR4","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1145\/1149114.1149119","volume":"7","author":"A Charlesworth","year":"2006","unstructured":"Charlesworth, A. (2006). Comprehending software correctness implies comprehending an intelligence-related limitation. ACM Transactions on Computational Logic, 7, 590\u2013612.","journal-title":"ACM Transactions on Computational Logic"},{"key":"9349_CR5","doi-asserted-by":"crossref","first-page":"1143","DOI":"10.1073\/pnas.50.6.1143","volume":"50","author":"P Cohen","year":"1963","unstructured":"Cohen, P. (1963). The independence of the continuum hypothesis. Proceedings of the National Academy of Sciences of the USA, 50, 1143\u20131148.","journal-title":"Proceedings of the National Academy of Sciences of the USA"},{"key":"9349_CR6","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A. (2006). Termination proofs for systems code. In Proceedings of the 2006 ACM SIGPLAN conference on programming language design and implementation, pp. 415\u2013426.","DOI":"10.1145\/1133981.1134029"},{"issue":"11","key":"9349_CR7","first-page":"12","volume":"38","author":"PM Dorin","year":"1995","unstructured":"Dorin, P. M., & Toal, R. J. (1995). Understanding noncomputability. Communications of the ACM, 38(11), 12.","journal-title":"Communications of the ACM"},{"issue":"8","key":"9349_CR8","doi-asserted-by":"crossref","first-page":"651","DOI":"10.2307\/2309339","volume":"66","author":"GE Forsythe","year":"1959","unstructured":"Forsythe, G. E. (1959). The role of numerical analysis in an undergraduate program. American Mathematical Monthly, 66(8), 651\u2013662.","journal-title":"American Mathematical Monthly"},{"key":"9349_CR9","volume-title":"Poor Richard\u2019s Almanac","author":"B Franklin","year":"1914","unstructured":"Franklin, B. (1914). Poor Richard\u2019s Almanac. Waterloo, IA: The U.S.C. Publishing Co."},{"key":"9349_CR10","doi-asserted-by":"crossref","DOI":"10.1201\/b10700","volume-title":"G\u00f6del\u2019s Theorem: An incomplete guide to its use and abuse","author":"T Franz\u00e9n","year":"2005","unstructured":"Franz\u00e9n, T. (2005). G\u00f6del\u2019s Theorem: An incomplete guide to its use and abuse. Wellesley, MA: A. K. Peters."},{"key":"9349_CR11","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K G\u00f6del","year":"1931","unstructured":"G\u00f6del, K. (1931). \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I. Monatshefte f\u00fcr Mathematik und Physik, 38, 173\u2013198.","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"9349_CR12","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1073\/pnas.25.4.220","volume":"25","author":"K G\u00f6del","year":"1939","unstructured":"G\u00f6del, K. (1939). Consistency proof for the generalized continuum hypothesis. Proceedings of the National Academy of Sciences of the USA, 25, 28\u201332.","journal-title":"Proceedings of the National Academy of Sciences of the USA"},{"key":"9349_CR13","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., & Xu, R.-G. (2008). Proving non-termination. In Proceedings of the 2008 ACM SIGPLAN-SIGACT principles of programming languages conference, pp. 147\u2013158.","DOI":"10.1145\/1328438.1328459"},{"key":"9349_CR14","volume-title":"The collected dialogues of Plato","author":"E Hamilton","year":"1961","unstructured":"Hamilton, E., & Cairns, H. (1961). The collected dialogues of Plato. Princeton, NJ: Princeton University Press."},{"issue":"11","key":"9349_CR15","first-page":"1395","volume":"55","author":"J Harrison","year":"2008","unstructured":"Harrison, J. (2008). Formal proof - theory and practice. Notices of the American Mathematical Society, 55(11), 1395\u20131406.","journal-title":"Notices of the American Mathematical Society"},{"key":"9349_CR16","volume-title":"An introduction to mathematical logic","author":"RE Hodel","year":"1995","unstructured":"Hodel, R. E. (1995). An introduction to mathematical logic. Boston: PWS Publishing Company."},{"key":"9349_CR17","volume-title":"G\u00f6del, Escher, Bach: An eternal golden braid","author":"D Hofstadter","year":"1979","unstructured":"Hofstadter, D. (1979). G\u00f6del, Escher, Bach: An eternal golden braid. New York: Basic Books."},{"key":"9349_CR18","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1038\/scientificamerican1282-18","volume":"247","author":"D Hofstadter","year":"1982","unstructured":"Hofstadter, D. (1982). Can inspiration be mechanized? Scientific American, 247, 18\u201334.","journal-title":"Scientific American"},{"issue":"4","key":"9349_CR19","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1112\/blms\/14.4.285","volume":"14","author":"L Kirby","year":"1982","unstructured":"Kirby, L., & Paris, J. (1982). Accessible independence results for Peano Arithmetic. Bulletin of the London Mathematical Society, 14(4), 285\u2013293.","journal-title":"Bulletin of the London Mathematical Society"},{"issue":"6","key":"9349_CR20","first-page":"707","volume":"61","author":"DE Knuth","year":"1973","unstructured":"Knuth, D. E. (1973). Computer science and its relation to mathematics. American Scientist, 61(6), 707\u2013713.","journal-title":"American Scientist"},{"key":"9349_CR21","volume-title":"Selected papers on computer science","author":"DE Knuth","year":"1996","unstructured":"Knuth, D. E. (1996). Selected papers on computer science. New York: Cambridge University Press."},{"key":"9349_CR22","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/S0004-3702(98)00052-6","volume":"104","author":"G LaForte","year":"1998","unstructured":"LaForte, G., Hayes, P. J., & Ford, K. M. (1998). Why G\u00f6del\u2019s Theorem cannot refute computationalism. Artificial Intelligence, 104, 265\u2013286.","journal-title":"Artificial Intelligence"},{"key":"9349_CR23","volume-title":"Big brain: The origins and future of human intelligence","author":"G Lynch","year":"2008","unstructured":"Lynch, G., & Granger, R. (2008). Big brain: The origins and future of human intelligence. New York: Macmillan."},{"key":"9349_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4872-9","volume-title":"Mathematics: Form and function","author":"S Mac Lane","year":"1986.","unstructured":"Mac Lane, S. (1986.). Mathematics: Form and function. New York: Springer."},{"key":"9349_CR25","first-page":"256","volume-title":"The third culture","author":"M Minsky","year":"1995","unstructured":"Minsky, M. (1995). Reply to Penrose\u2019s \u201cConsciousness involves noncomputable ingredients\u201d. In J. Brockman (Ed.), The third culture (pp. 256\u2013257). New York: Simon and Schuster."},{"issue":"11","key":"9349_CR26","first-page":"104","volume":"13","author":"H Moravec","year":"1992","unstructured":"Moravec, H. (1992). Minds with mobility [an interview]. Discover, 13(11), 104\u2013106.","journal-title":"Discover"},{"key":"9349_CR27","volume-title":"Artificial intelligence: A modern approach","author":"SJ Russell","year":"2010","unstructured":"Russell, S. J., & Norvig, P. (2010). Artificial intelligence: A modern approach (3rd ed.). Englewood Cliffs, NJ: Prentice-Hall.","edition":"3"},{"key":"9349_CR28","unstructured":"Turing, A. M. (1936). On computable numbers with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 42, Ser. 2, 230\u2013265 (a correction 43 (1937), 544\u2013546)."},{"key":"9349_CR29","unstructured":"Turing, A. M. (1986). Lecture to the London Mathematical Society on 20 February 1947. In A. M. Turing\u2019s ACE report of 1946 and other papers (pp. 106\u2013124). Cambridge, MA: MIT Press."},{"key":"9349_CR30","volume-title":"A course in combinatorics","author":"JH Lint van","year":"1992","unstructured":"van Lint, J. H., & Wilson, R. M. (1992). A course in combinatorics. New York: Cambridge University Press."},{"key":"9349_CR31","volume-title":"Reflections on Kurt G\u00f6del","author":"H Wang","year":"1987","unstructured":"Wang, H. (1987). Reflections on Kurt G\u00f6del. Cambridge, MA: MIT Press."},{"key":"9349_CR32","doi-asserted-by":"crossref","first-page":"443","DOI":"10.2307\/2118559","volume":"131","author":"AJ Wiles","year":"1995","unstructured":"Wiles, A. J. (1995). Modular elliptic curves and Fermat\u2019s last theorem. Annals of Mathematics, 131, 443\u2013551.","journal-title":"Annals of Mathematics"}],"container-title":["Minds and Machines"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11023-014-9349-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11023-014-9349-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11023-014-9349-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,16]],"date-time":"2019-08-16T21:43:08Z","timestamp":1565991788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11023-014-9349-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,11]]}},"alternative-id":["9349"],"URL":"https:\/\/doi.org\/10.1007\/s11023-014-9349-3","relation":{},"ISSN":["0924-6495","1572-8641"],"issn-type":[{"value":"0924-6495","type":"print"},{"value":"1572-8641","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11]]}}}