{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T13:07:57Z","timestamp":1768568877478,"version":"3.49.0"},"reference-count":17,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2006,7,1]],"date-time":"2006-07-01T00:00:00Z","timestamp":1151712000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2006,7]]},"abstract":"<jats:p>\n            This article applies mathematical logic to obtain a rigorous foundation for previous inherently nonrigorous results and also extends those previous results. Roughly speaking, our main theorem states: any agent A that comprehends the correctness-related properties of software\n            <jats:italic>S<\/jats:italic>\n            also comprehends an intelligence-related limitation of\n            <jats:italic>S<\/jats:italic>\n            . The theorem treats the output of\n            <jats:italic>S<\/jats:italic>\n            , if any, as an attempt at solving a halting problem. Previous nonrigorous attempts to obtain similar theorems depend on infallibility assumptions on both the agent and the software. The hypothesis that intelligent agents and intelligent software must be infallible has been widely questioned. In addition, recent work by others has determined that well-known previous attempts use a fallacious form of reasoning; that is, the same form of reasoning can yield paradoxical results. Our main theorem avoids infallibility assumptions on both the agent and the software. In addition, our proof is rigorous, in the sense that in principle one can carry it out in Zermelo-Fraenkel set theory. The software correctness framework considered in the main theorem is that of Hoare logic.\n          <\/jats:p>","DOI":"10.1145\/1149114.1149119","type":"journal-article","created":{"date-parts":[[2006,10,18]],"date-time":"2006-10-18T18:11:32Z","timestamp":1161195092000},"page":"590-612","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Comprehending software correctness implies comprehending an intelligence-related limitation"],"prefix":"10.1145","volume":"7","author":[{"given":"Arthur","family":"Charlesworth","sequence":"first","affiliation":[{"name":"University of Richmond, Richmond, VA"}]}],"member":"320","published-online":{"date-parts":[[2006,7]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_2_2_2_1","volume-title":"Impossibility: The Limits of Science and the Science of Limits","author":"Barrow J. D.","year":"1998"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5840\/monist196751112"},{"key":"e_1_2_2_4_1","first-page":"6","article-title":"Mind out of matter: A review of Shadows of the Mind, by Roger","volume":"275","author":"Chalmers D. J.","year":"1995","journal-title":"Penrose. Sci. Amer."},{"key":"e_1_2_2_5_1","unstructured":"Enderton H. B. 1972. A Mathematical Introduction to Logic. Academic Press New York NY.  Enderton H. B. 1972. A Mathematical Introduction to Logic. Academic Press New York NY."},{"key":"e_1_2_2_6_1","volume-title":"Kurt G\u00f6del: Collected Works","author":"G\u00f6del K."},{"key":"e_1_2_2_7_1","volume-title":"Kurt G\u00f6del: Collected Works","author":"G\u00f6del K."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(98)00052-6"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0031819100057983"},{"key":"e_1_2_2_10_1","first-page":"17","article-title":"{STAR} Penrose is wrong","volume":"2","author":"McDermott D.","year":"1995","journal-title":"Psyche"},{"key":"e_1_2_2_11_1","volume-title":"The Third Culture","author":"Minsky M."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Penrose R. 1989. The Emperor's New Mind. Oxford University Press New York NY.  Penrose R. 1989. The Emperor's New Mind. Oxford University Press New York NY.","DOI":"10.1093\/oso\/9780198519737.001.0001"},{"key":"e_1_2_2_14_1","unstructured":"Penrose R. 1994. Shadows of the Mind. Oxford University Press New York NY.  Penrose R. 1994. Shadows of the Mind. Oxford University Press New York NY."},{"key":"e_1_2_2_15_1","unstructured":"Rucker R. 1982. Infinity and the Mind. Birkhauser Boston MA.  Rucker R. 1982. Infinity and the Mind. Birkhauser Boston MA."},{"key":"e_1_2_2_16_1","unstructured":"Shoenfield J. R. 1967. Mathematical Logic. Addison-Wesley Reading MA.  Shoenfield J. R. 1967. Mathematical Logic. Addison-Wesley Reading MA."},{"key":"e_1_2_2_17_1","unstructured":"Turing A. M. 1986. Lecture to the London Mathematical Society on 20 February 1947. In A. M. Turing's ACE Report of 1946 and Other Papers B. E. Carpenter and R. W. Doran Eds. MIT Press Cambridge MA 106--124.  Turing A. M. 1986. Lecture to the London Mathematical Society on 20 February 1947. In A. M. Turing's ACE Report of 1946 and Other Papers B. E. Carpenter and R. W. Doran Eds. MIT Press Cambridge MA 106--124."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1149114.1149119","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1149114.1149119","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:13Z","timestamp":1750264273000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1149114.1149119"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,7]]},"references-count":17,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,7]]}},"alternative-id":["10.1145\/1149114.1149119"],"URL":"https:\/\/doi.org\/10.1145\/1149114.1149119","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,7]]},"assertion":[{"value":"2006-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}