{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:51:01Z","timestamp":1743007861903,"version":"3.40.3"},"publisher-location":"Dordrecht","reference-count":46,"publisher":"Springer Netherlands","isbn-type":[{"type":"print","value":"9789400765337"},{"type":"electronic","value":"9789400765344"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-94-007-6534-4_9","type":"book-chapter","created":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T08:27:22Z","timestamp":1372667242000},"page":"147-170","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Checking Proofs"],"prefix":"10.1007","author":[{"given":"Jesse","family":"Alama","sequence":"first","affiliation":[]},{"given":"Reinhard","family":"Kahle","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,5,25]]},"reference":[{"key":"9_CR1","first-page":"439","volume":"21","author":"K. Appel","year":"1977","unstructured":"Appel, K., & Haken, W. (1977). Every planar map is four-colorable. Illinois Journal of Mathematics, 21, 439\u2013567.","journal-title":"Illinois Journal of Mathematics"},{"issue":"2","key":"9_CR2","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s11023-007-9063-5","volume":"17","author":"K. Arkoudas","year":"2007","unstructured":"Arkoudas, K., & Bringsjord, S. (2007). Computers, justification, and mathematical knowledge. Minds and Machines, 17(2), 185\u2013202.","journal-title":"Minds and Machines"},{"issue":"7","key":"9_CR3","first-page":"736","volume":"51","author":"M. Aschbacher","year":"2004","unstructured":"Aschbacher, M. (2004). The status of the classification of the finite simple groups. Notices of the American Mathematical Society, 51(7), 736\u2013740.","journal-title":"Notices of the American Mathematical Society"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s11229-005-4064-5","volume":"153","author":"J. Avigad","year":"2006","unstructured":"Avigad, J. (2006). Mathematical method and proof. Synthese, 153, 105\u2013149.","journal-title":"Synthese"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1093\/philmat\/12.2.81","volume":"12","author":"J. Azzouni","year":"2004","unstructured":"Azzouni, J. (2004). The derivation-indicator view of mathematical practice. Philosophia Mathematica, 12, 81\u2013106.","journal-title":"Philosophia Mathematica"},{"key":"9_CR6","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s11229-004-6221-7","volume":"148","author":"O. B. Bassler","year":"2006","unstructured":"Bassler, O.\u00a0B. (2006). The surveyability of mathematical proof: A historical perspective. Synthese, 148, 99\u2013133.","journal-title":"Synthese"},{"key":"9_CR7","first-page":"1","volume-title":"Handbook of proof theory","author":"S. Buss","year":"1998","unstructured":"Buss, S. (1998). An introduction to proof theory. In S. Buss (Ed.), Handbook of proof theory, volume 137 of studies in logic and the foundations of mathematics (pp. 1\u201378). Amsterdam: Elsevier."},{"issue":"14","key":"9_CR8","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1093\/mind\/IV.14.278","volume":"4","author":"L. Carroll","year":"1895","unstructured":"Carroll, L. (1895). What the tortoise said to Achilles. Mind, 4(14), 278\u2013280.","journal-title":"Mind"},{"key":"9_CR9","first-page":"530","volume-title":"Proceedings of the 7th international joint conference on artificial intelligence (IJCAI)","author":"M. Davis","year":"1981","unstructured":"Davis, M. (1981). Obvious logical inferences. In Proceedings of the 7th international joint conference on artificial intelligence (IJCAI) (pp. 530\u2013531). Los Angeles, CA: William Kaufmann."},{"key":"9_CR10","unstructured":"de\u00a0Bruijn, N. (1980). A survey of the project Automath. In J.\u00a0R. Hindley & J.\u00a0P. Seldin (Eds.), To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism. London: Academic Press."},{"issue":"5","key":"9_CR11","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"R. De Millo","year":"1979","unstructured":"De\u00a0Millo, R., Lipton, R.\u00a0J., & Perlis, A.\u00a0J. (1979). Social processes and proofs of theorems and programs. Communications of the ACM, 22(5), 271\u2013280.","journal-title":"Communications of the ACM"},{"issue":"12","key":"9_CR12","doi-asserted-by":"publisher","first-page":"803","DOI":"10.2307\/2025806","volume":"77","author":"M. Detlefsen","year":"1980","unstructured":"Detlefsen, M., & Luker, M. (1980). The four-color theorem and mathematical proof. Journal of Philosophy, 77(12), 803\u2013820.","journal-title":"Journal of Philosophy"},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1023\/A:1022131513275","volume":"134","author":"D. Fallis","year":"2003","unstructured":"Fallis, D. (2003). Intentional gaps in mathematical proofs. Synthese, 134, 45\u201369.","journal-title":"Synthese"},{"issue":"11","key":"9_CR14","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G. (2008). Formal proof\u2014The four color theorem. Notices of the American Mathematical Society, 55(11), 1382\u20131393.","journal-title":"Notices of the American Mathematical Society"},{"issue":"2","key":"9_CR15","first-page":"153","volume":"3","author":"A. Grabowski","year":"2010","unstructured":"Grabowski, A., Korni\u0142owicz, A., & Naumowicz, A. (2010). Mizar in a nutshell. Journal of Formalized Reasoning, 3(2), 153\u2013245.","journal-title":"Journal of Formalized Reasoning"},{"issue":"3","key":"9_CR16","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.4007\/annals.2005.162.1065","volume":"162","author":"T. C. Hales","year":"2005","unstructured":"Hales, T. C. (2005). A proof of the Kepler conjecture. Annals of Mathematics, 162(3), 1063\u20131185.","journal-title":"Annals of Mathematics"},{"issue":"11","key":"9_CR17","first-page":"1370","volume":"55","author":"T. C. Hales","year":"2008","unstructured":"Hales, T.\u00a0C. (2008). Formal proof. Notices of the American Mathematical Society, 55(11), 1370\u20131380.","journal-title":"Notices of the American Mathematical Society"},{"key":"9_CR18","volume-title":"An introduction to the theory of numbers","author":"G. H. Hardy","year":"1960","unstructured":"Hardy, G.\u00a0H., & Wright, E.\u00a0M. (1960). An introduction to the theory of numbers (4th ed.). Oxford: Oxford University Press.","edition":"4"},{"issue":"11","key":"9_CR19","first-page":"1395","volume":"55","author":"J. Harrison","year":"2008","unstructured":"Harrison, J. (2008). Formal proof\u2014Theory and practice. Notices of the American Mathematical Society, 55(11), 1395\u20131406.","journal-title":"Notices of the American Mathematical Society"},{"key":"9_CR20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of practical logic and automated reasoning","author":"J. Harrison","year":"2009","unstructured":"Harrison, J. (2009). Handbook of practical logic and automated reasoning. Cambridge: Cambridge University Press."},{"issue":"6","key":"9_CR21","doi-asserted-by":"publisher","first-page":"929","DOI":"10.1177\/0306312703336005","volume":"33","author":"B. Heintz","year":"2003","unstructured":"Heintz, B. (2003). When is a proof a proof? Social Studies of Science, 33(6), 929\u2013943.","journal-title":"Social Studies of Science"},{"key":"9_CR22","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139171472","volume-title":"Proofs and refutations: The logic of mathematical discovery (edited by J. Worrall & E. Zahar)","author":"I. Lakatos","year":"1976","unstructured":"Lakatos, I. (1976). Proofs and refutations: The logic of mathematical discovery (edited by J.\u00a0Worrall & E. Zahar). Cambridge: Cambridge University Press."},{"key":"9_CR23","volume-title":"Philosophical perspectives on mathematical practice","author":"B. L\u00f6we","year":"2010","unstructured":"L\u00f6we, B., M\u00fcller, T., & M\u00fcller-Hill, E. (2010). Mathematical knowledge as a case study in empirical philosophy of mathematics. In B. van Kerkhove, J. de\u00a0Vuyst, & J.\u00a0P. van Bendegem, (Eds.), Philosophical perspectives on mathematical practice. London: College Publications."},{"issue":"1","key":"9_CR24","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1177\/030631299029001002","volume":"29","author":"D. MacKenzie","year":"1999","unstructured":"MacKenzie, D. (1999). Slaying the Kraken: The sociohistory of a mathematical proof. Social Studies of Science, 29(1), 7\u201360.","journal-title":"Social Studies of Science"},{"key":"9_CR25","volume-title":"Mechanizing proof: Computing, risk, and trust","author":"D. MacKenzie","year":"2004","unstructured":"MacKenzie, D. (2004). Mechanizing proof: Computing, risk, and trust. Cambridge, MA: MIT Press."},{"key":"9_CR26","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-94-015-9558-2_8","volume-title":"Growth of mathematical knowledge","author":"P. Mancosu","year":"2000","unstructured":"Mancosu, P. (2000). On mathematical explanation. In E. Grosholz & H. Berger (Eds.), Growth of mathematical knowledge (pp. 103\u2013119). Dordrecht: Kluwer."},{"key":"9_CR27","first-page":"3","volume":"4","author":"R. Matuszewski","year":"2005","unstructured":"Matuszewski, R., & Rudnicki, P. (2005). Mizar: The first 30 years. Mechanized Mathematics and Its Applications, 4, 3\u201324.","journal-title":"Mechanized Mathematics and Its Applications"},{"issue":"3","key":"9_CR28","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W. (1997). Solution of the Robbins problem. Journal of Automated Reasoning, 19(3), 263\u2013276.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR29","volume-title":"The shaping of deduction in Greek mathematics: A study in cognitive history","author":"R. Netz","year":"2003","unstructured":"Netz, R. (2003). The shaping of deduction in Greek mathematics: A study in cognitive history. Cambridge: Cambridge University Press."},{"key":"9_CR30","volume-title":"Complexity of proofs and their transformations in axiomatic theories, volume 128 of translations of mathematical monographs (A. Bochman, Trans. from the original Russian manuscript, translation edited by D. Louvish)","author":"V. P. Orevkov","year":"1993","unstructured":"Orevkov, V.\u00a0P. (1993). Complexity of proofs and their transformations in axiomatic theories, volume 128 of translations of mathematical monographs (A. Bochman, Trans. from the original Russian manuscript, translation edited by D. Louvish). Providence, RI: American Mathematical Society."},{"key":"9_CR31","unstructured":"Portoraro, F. (2008). Automated reasoning. In E.\u00a0N. Zalta (Ed.), Stanford encyclopedia of philosophy. Fall 2008 Edition. http:\/\/plato.stanford.edu\/archives\/fall2008\/entries\/reasoning-automated\/."},{"key":"9_CR32","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-88-470-0784-0_5","volume-title":"Deduction, computation, experiment: Exploring the effectiveness of proof","author":"D. Prawitz","year":"2008","unstructured":"Prawitz, D. (2008). Proofs verifying programs and programs producing proofs: A conceptual analysis. In R. Lupacchini & G. Corsi (Ed.), Deduction, computation, experiment: Exploring the effectiveness of proof (pp. 81\u201394). Milan: Springer."},{"issue":"3","key":"9_CR33","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1093\/philmat\/nkm023","volume":"15","author":"Y. Rav","year":"2007","unstructured":"Rav, Y. (2007). A critique of a formalist-mechanist version of the justification of arguments in mathematicians\u2019 proof practices. Philosophia Mathematica, 15(3), 291\u2013320.","journal-title":"Philosophia Mathematica"},{"key":"9_CR34","unstructured":"Rehmeyer, J. (2008). How to (really) trust a mathematical proof. Science News. Accessed May 2013. http:\/\/www.sciencenews.org\/view\/generic\/id\/38623\/title\/How_to_(really)_trust_a_mathematical_proof."},{"key":"9_CR35","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/jctb.1997.1750","volume":"70","author":"N. Robertson","year":"1997","unstructured":"Robertson, N., Sanders, D.\u00a0P., Seymour, P.\u00a0D., & Thomas, R. (1997). The four colour theorem. Journal of Combinatorial Theory. Series B, 70, 2\u201344.","journal-title":"Journal of Combinatorial Theory. Series B"},{"issue":"4","key":"9_CR36","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/BF00247436","volume":"3","author":"P. Rudnicki","year":"1987","unstructured":"Rudnicki, P. (1987). Obvious inferences. Journal of Automated Reasoning, 3(4), 383\u2013393.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR37","volume-title":"Foreword. In F. Wiedijk (Ed.), The seventeen provers of the world, volume 3600 of lecture notes in computer science (pp. vii\u2013xii)","author":"D. Scott","year":"2006","unstructured":"Scott, D. (2006). Foreword. In F. Wiedijk (Ed.), The seventeen provers of the world, volume 3600 of lecture notes in computer science (pp. vii\u2013xii). Berlin: Springer."},{"issue":"12","key":"9_CR38","doi-asserted-by":"publisher","first-page":"797","DOI":"10.2307\/2025805","volume":"77","author":"P. Teller","year":"1980","unstructured":"Teller, P. (1980). Computer proof. Journal of Philosophy, 77(12), 797\u2013803.","journal-title":"Journal of Philosophy"},{"key":"9_CR39","unstructured":"Thomas, R. (2007). The four color theorem. Accessed May 2013. http:\/\/www.math.gatech.edu\/~thomas\/FC\/fourcolor.html."},{"key":"9_CR40","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511840005","volume-title":"The uses of argument","author":"S. E. Toulmin","year":"2003","unstructured":"Toulmin, S.\u00a0E. (2003). The uses of argument (updated ed.). Cambridge: Cambridge University Press."},{"issue":"2","key":"9_CR41","doi-asserted-by":"publisher","first-page":"57","DOI":"10.2307\/2025976","volume":"76","author":"T. Tymoczko","year":"1979","unstructured":"Tymoczko, T. (1979). The four-color problem and its philosophical significance. Journal of Philosophy, 76(2), 57\u201383.","journal-title":"Journal of Philosophy"},{"key":"9_CR42","doi-asserted-by":"crossref","unstructured":"van Bendegem, J.\u00a0P. (1988). Non-formal properties of real mathematical proofs. In J. Leplin, A. Fine, & M. Forbes (Eds.), PSA: Proceedings of the biennial meeting of the philosophy of science association (Vol. 1, pp. 249\u2013254). East Lansing, MI: Philosophy of Science Association (Contributed papers).","DOI":"10.1086\/psaprocbienmeetp.1988.1.192992"},{"key":"9_CR43","first-page":"398","volume-title":"CADE","author":"K. Verchinine","year":"2007","unstructured":"Verchinine, K., Lyaletski, A.\u00a0V., & Paskevich, A. (2007). System for automated deduction (SAD): A tool for proof verification. In F. Pfenning (Ed.), CADE, volume 4603 of lecture notes in computer science (pp. 398\u2013403). Berlin: Springer."},{"issue":"1","key":"9_CR44","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1147\/rd.41.0002","volume":"4","author":"H. Wang","year":"1960","unstructured":"Wang, H. (1960). Toward mechanical mathematics. IBM Journal of Research and Development, 4(1), 2\u201322.","journal-title":"IBM Journal of Research and Development"},{"volume-title":"The seventeen provers of the world, volume 3600 of lecture notes in computer science","year":"2006","key":"9_CR45","unstructured":"Wiedijk, F. (Ed.). (2006). The seventeen provers of the world, volume 3600 of lecture notes in computer science. Berlin: Springer."},{"issue":"11","key":"9_CR46","first-page":"1408","volume":"55","author":"F. Wiedijk","year":"2008","unstructured":"Wiedijk, F. (2008). Formal proof\u2014Getting started. Notices of the American Mathematical Society, 55(11), 1408\u20131414.","journal-title":"Notices of the American Mathematical Society"}],"container-title":["The Argument of Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-94-007-6534-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T15:02:52Z","timestamp":1680793372000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-94-007-6534-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9789400765337","9789400765344"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-94-007-6534-4_9","relation":{},"subject":[],"published":{"date-parts":[[2013]]},"assertion":[{"value":"25 May 2013","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}