{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T05:46:23Z","timestamp":1741153583521,"version":"3.38.0"},"publisher-location":"Dordrecht","reference-count":64,"publisher":"Springer Netherlands","isbn-type":[{"type":"print","value":"9789400700796"},{"type":"electronic","value":"9789400700802"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-94-007-0080-2_3","type":"book-chapter","created":{"date-parts":[[2011,4,1]],"date-time":"2011-04-01T18:04:08Z","timestamp":1301681048000},"page":"35-52","source":"Crossref","is-referenced-by-count":0,"title":["What Is a Proof?"],"prefix":"10.1007","author":[{"given":"John N.","family":"Crossley\u00a7","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,3,10]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1215\/ijm\/1256049011","volume":"21","author":"I. Kenneth","year":"1977","unstructured":"Kenneth I. Appel and Wolfgang Haken. Every planar map is four colorable. I. Discharging, Illinois J. Math., 21: 429\u2013490, 1977.","journal-title":"Illinois J. Math."},{"key":"3_CR2","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1215\/ijm\/1256049012","volume":"21","author":"I. Kenneth","year":"1977","unstructured":"Kenneth I. Appel and Wolfgang Haken. Every planar map is four colorable. II. Reducibility, Illinois J. Math., 21: 491\u2013567, 1977.","journal-title":"Illinois J. Math."},{"key":"3_CR3","unstructured":"Aristotle. On Interpretation. In [51], pages 40\u201364."},{"key":"3_CR4","unstructured":"Aristotle. Posterior Analyics. In [51], pages 110\u2013186."},{"key":"3_CR5","unstructured":"Aristotle. Prior Analyics. In [51], pages 65\u2013106."},{"issue":"7","key":"3_CR6","first-page":"736","volume":"51","author":"M. Aschbacher","year":"2004","unstructured":"Aschbacher M. The status of the classification of finite simple groups, Notices of the Amer. Math. Soc., 51(7): 736\u2013740, 2004.","journal-title":"Notices of the Amer. Math. Soc."},{"key":"3_CR7","volume-title":"The Lambda Calculus, Its Syntax and Semantics","author":"P. H. Barendregt","year":"1995","unstructured":"Barendregt P. H. The Lambda Calculus, Its Syntax and Semantics. North Holland Publishing Company, Amsterdam, 1995."},{"key":"3_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of Constructive Mathematics","author":"M. J. Beeson","year":"1985","unstructured":"Beeson M. J. Foundations of Constructive Mathematics. Number 6 in Ergebnisse der Mathematik und ihren Grenzgebiete; 3. Folge. Springer, Berlin, 1985."},{"key":"3_CR9","volume-title":"General Systems Theory: Foundations, Development, Applications","author":"L. v. Bertalanffy","year":"1968","unstructured":"Bertalanffy L. v. General Systems Theory: Foundations, Development, Applications. George Braziller, New York, NY, 1968."},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Bolyai J. The Science of Absolute of Space: Independent of the Truth or Falsity of Euclid\u2019s Axiom XI, translated by G. Halsted 4th ed. The University of Texas, Austin, 1896.","DOI":"10.5962\/bhl.title.18017"},{"key":"3_CR11","volume-title":"Theory of Groups of Finite Order","author":"W. Burnside","year":"2004","unstructured":"Burnside W. Theory of Groups of Finite Order, 2nd ed. Dover Phoenix Editions, New York, NY, 2004. This edition was originally published in 1911.","edition":"2"},{"key":"3_CR12","unstructured":"Buss S. R. Bounded Arithmetic. Bibliopolis, Naples, 1986. A revised version of his PhD thesis."},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0168-0072(98)00030-X","volume":"96","author":"S. R. Buss","year":"1999","unstructured":"Buss S. R. Bounded arithmetic, proof complexity and two papers of Parikh, Ann. Pure Appl. Logic, 96: 43\u201355, 1999.","journal-title":"Ann. Pure Appl. Logic"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"584","DOI":"10.1073\/pnas.20.11.584","volume":"20","author":"A. Church","year":"1934","unstructured":"Church A. An unsolvable problem of elementary number theory, Proc. Nat. Acad. Sci. USA, 20: 584\u2013590, 1934.","journal-title":"Proc. Nat. Acad. Sci. USA"},{"key":"3_CR15","volume-title":"La logique de Leibniz d\u2019apr\u2018es des documents in\u00e9dits","author":"L. Couturat","year":"1901","unstructured":"Couturat L. La logique de Leibniz d\u2019apr\u2018es des documents in\u00e9dits. Feliz Alcan, Paris, 1901. Reprinted Georg Olms, Hildesheim, 1961."},{"key":"3_CR16","volume-title":"Opuscules et fragments in\u00e9dits de Leibniz","author":"L. Couturat","year":"1903","unstructured":"Couturat L. Opuscules et fragments in\u00e9dits de Leibniz. Feliz Alcan, Paris, 1903. Reprinted Georg Olms, Hildesheim, 1961."},{"key":"3_CR17","unstructured":"Crossley J. N. What is a logic? Presented at the International Conference on Logic, Navya-Ny\u0101ya and Applications: A Homage to Bimal Krishna Matilal, January 2007."},{"key":"3_CR18","unstructured":"Crossley J. N. What is the difference between proofs and programs? Lecture at the First International Conference on Logic and and its application to other disciplines, IIT Bombay, 2005, submitted for publication."},{"key":"3_CR19","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1080\/00048407312341051","volume":"51","author":"J. N. Crossley","year":"1973","unstructured":"Crossley J. N. A note on Cantor\u2019s theorem and Russell\u2019s paradox, Austral. J. Phil., 51: 70\u201371, 1973.","journal-title":"Austral. J. Phil."},{"key":"3_CR20","first-page":"81","volume":"11","author":"J. N. Crossley","year":"1988","unstructured":"Crossley J. N. Fifty years of computability, Southeast Asian Bull. Math., 11: 81\u201399, 1988.","journal-title":"Southeast Asian Bull. Math."},{"key":"3_CR21","first-page":"234","volume-title":"Mathematical Problems from Applied Logic. New Logics for XXI Century (International Mathematical Series)","author":"J. N. Crossley","year":"2005","unstructured":"Crossley J. N. Samsara. In D. Gabbay, S. S. Goncharov, and M. Zakharyaschev, editors, Mathematical Problems from Applied Logic. New Logics for XXI Century (International Mathematical Series), pages 234\u2013276. Springer, Berlin, 2005."},{"key":"3_CR22","first-page":"259","volume":"1","author":"J. N. Crossley","year":"1994","unstructured":"Crossley J. N., Mathai G. L., and Seely R. A. G. A logical calculus for polynomial-time realizability, Methods Logic Comput. Sci., 1: 259\u2013278, 1994.","journal-title":"Methods Logic Comput. Sci."},{"key":"3_CR23","first-page":"183","volume":"1","author":"J. N. Crossley","year":"1994","unstructured":"Crossley J. N., and Remmel J. B. Proofs, programs and run times, Methods Logic Comput. Sci., 1: 183\u2013215, 1994.","journal-title":"Methods Logic Comput. Sci."},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"345","DOI":"10.2307\/2371045","volume":"58","author":"H. B. Curry","year":"1936","unstructured":"Curry H. B. Functionality in combinatory logic, Am. J. Math., 58: 345\u2013363, 1936.","journal-title":"Am. J. Math."},{"key":"3_CR25","volume-title":"Combinatory Logic","author":"H. B. Curry","year":"1958","unstructured":"Curry H. B., and Feys R. Combinatory Logic, vol. 1. North-Holland, Amsterdam, 1958."},{"key":"3_CR26","volume-title":"The Finite Element Method","author":"A. J. Davies","year":"1980","unstructured":"Davies A. J. The Finite Element Method. Oxford University Press, Oxford, 1980."},{"key":"3_CR27","unstructured":"Devlin K. Devlin\u2019s Angle: When is a proof? In MAA Online. Mathematical Association of America, June 2003. http:\/\/www.maa.org\/devlin\/devlin_06_03.html , accessed 8.iii.05"},{"key":"3_CR28","unstructured":"Dipert R. R. Logic, history of [electronic version]. In Encyclopdia Britannica Online, 2006. http:\/\/search.eb.com\/eb\/article-65939 , accessed 1.vii.06"},{"key":"3_CR29","unstructured":"Dutens L., editor. Gothofredi Guillelmi Leibnitii Opera Omnia: Nunc prima collecta, in classes distributa, prfationibus & indicibus exornata, studio Ludovici Dutens \u2026. Apud Fratres de Tournes, Geneva, 1768. 6 vols., reprinted Georg Olms, Hildesheim, 1989."},{"volume-title":"Die philosophische Schriften von Gottfried Wilhelm Leibniz","year":"1978","key":"3_CR30","unstructured":"Gerhardt C. I., editor. Die philosophische Schriften von Gottfried Wilhelm Leibniz, 7 vols. Georg Olms, Hildesheim, 1978."},{"key":"3_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J. Y. Girard","year":"1987","unstructured":"Girard J. Y. Linear logic, Theor. Comput. Sci., 50: 1\u2013102, 1987.","journal-title":"Theor. Comput. Sci."},{"key":"3_CR32","volume-title":"Proof theory and Logical Complexity","author":"J. Y. Girard","year":"1987","unstructured":"Girard J. Y. Proof theory and Logical Complexity. Bibliopolis, Naples, 1987."},{"key":"3_CR33","volume-title":"Proofs and Types","author":"J. Y. Girard","year":"1989","unstructured":"Girard J. Y., Lafont Y., and Taylor P. Proofs and Types. Cambridge University Press, Cambridge, 1989."},{"key":"3_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(92)90386-T","volume":"97","author":"J. Y. Girard","year":"1992","unstructured":"Girard J. Y., Scott P. J., and Seely R. A. G. Bounded linear logic: a modular approach to polynomial-time computability, Theor. Comput. Sci., 97: 1\u201366, 1992.","journal-title":"Theor. Comput. Sci."},{"key":"3_CR35","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K. G\u00f6del","year":"1931","unstructured":"G\u00f6del K. \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme, Monatshefte f\u00fcr Mathematik und Physik, 38: 173\u2013198, 1931.","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"3_CR36","unstructured":"Gonthier G. A computer-checked proof of the Four Colour Theorem. http:\/\/research . microsoft.com\/%7Egonthier\/4colproof.pdf, accessed 13.xii.06"},{"key":"3_CR37","volume-title":"A Short History of Greek Mathematics","author":"J. Gow","year":"1968","unstructured":"Gow J. A Short History of Greek Mathematics. Chelsea Pub. Co., New York, NY, 1968. Revised edn."},{"key":"3_CR38","volume-title":"The Thirteen Books of Euclid\u2019s Elements","year":"1925","unstructured":"Heath T. L., editor. The Thirteen Books of Euclid\u2019s Elements, 2nd ed. Cambridge University Press, Cambridge, 1925. Reprinted, Dover Books, New York, 1956.","edition":"2"},{"key":"3_CR39","unstructured":"Hilbert D. On the foundations of logic and arithmetic, 1904. In [15], pages 129\u2013138."},{"key":"3_CR40","unstructured":"Hilbert D. The foundations of mathematics, 1927. In [15], pages 464\u2013479."},{"key":"3_CR41","volume-title":"Foundations of Geometry","author":"D. Hilbert","year":"1971","unstructured":"Hilbert D. Foundations of Geometry, 2nd ed., Open Court, La Salle, IL, 1971. Taken from the 10th German edn.","edition":"2"},{"key":"3_CR42","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"W. Howard","year":"1969","unstructured":"Howard W. The formulae-as-types notion of construction. In J. R. Hindley and J. Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479\u2013490. Academic Press, New York, NY, 1969."},{"key":"3_CR43","first-page":"193","volume-title":"Proceedings of the 7th and 8th Asian Logic Conferences, Chongqing, China, 29 August \u2013 2 September 2002","author":"J. S. Jeavons","year":"2003","unstructured":"Jeavons J. S., Poernomo I., Basit B., and Crossley J. N. A layered approach to extracting programs from proofs with an application in Graph Theory. In R. Downey, D. Decheng, T. S. Ping, Q. Y. Hui, and M. Yasugi, editors, Proceedings of the 7th and 8th Asian Logic Conferences, Chongqing, China, 29 August \u2013 2 September 2002, pages 193\u2013222, Singapore, 2003. Singapore University Press and World Scientific."},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Lakatos I. In J. Worrall and E. Zahar, editors, Proofs and Refutations: The Logic of Mathematical Discovery. Cambridge University Press, Cambridge, New York, 1976.","DOI":"10.1017\/CBO9781139171472"},{"key":"3_CR45","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/S0049-237X(08)70754-7","volume-title":"Intuitionism and proof theory; Proceedings of the Summer Conference at Buffalo, NY, 1968","author":"H. Lauchli","year":"1970","unstructured":"Lauchli H. An abstract notion of realizability for which intuitionistic predicate calculus is complete. In A. Kino, J. Myhill, and R. E. Vesley, editors, Intuitionism and proof theory; Proceedings of the Summer Conference at Buffalo, NY, 1968, pages 227\u2013234. North Holland Publishing Company, Amsterdam, 1970."},{"key":"3_CR46","first-page":"228","volume-title":"Die philosophische Schriften von Gottfried Wilhelm Leibniz","author":"G. W. Leibniz","year":"1961","unstructured":"Leibniz G. W. XIX. [Non inelegans specimen demonstrandi in abstractis]. In C. I. Gerhardt, editor, Die philosophische Schriften von Gottfried Wilhelm Leibniz, vol. VII, pages 228\u2013235. Georg Olms, Hildesheim, 1961. Reprint of the 1890 Berlin edition."},{"key":"3_CR47","volume-title":"Heritage of European Mathematics","author":"N. I. Lobachevsky","year":"2010","unstructured":"Lobachevsky N. I. Pangeometry, 1855 translated by A. Papadopoulos. Heritage of European Mathematics. European Mathematical Society (EMS), Z\u00fcrich, 2010."},{"key":"3_CR48","first-page":"63","volume":"LXXXIV","author":"J. R. Lucas","year":"1983","unstructured":"Lucas J. R. Mathematical tennis, Proceedings of the Aristotelian Society, n.s. LXXXIV: 63\u201372, 1983\/4.","journal-title":"Proceedings of the Aristotelian Society"},{"key":"3_CR49","volume-title":"Perception: An Essay on Classical Indian Theories of Knowledge","author":"B. K. Matilal","year":"1986","unstructured":"Matilal B. K. Perception: An Essay on Classical Indian Theories of Knowledge. Clarendon Press, Oxford, 1986."},{"key":"3_CR50","unstructured":"Maurolico F. Arithmeticorum libri duo. In Opuscula Mathematica. Francisci, Venice, 1575."},{"volume-title":"The Basic Works of Aristotle","year":"1941","key":"3_CR51","unstructured":"McKeon R. P., editor. The Basic Works of Aristotle. Random House, New York, NY, 1941."},{"key":"3_CR52","volume-title":"Introduction to Mathematical Logic","author":"E. Mendelson","year":"1997","unstructured":"Mendelson, E. Introduction to Mathematical Logic, 4th ed. Chapman & Hall, Boca Raton, FL, 1997.","edition":"4"},{"key":"3_CR53","doi-asserted-by":"crossref","unstructured":"Nerode A., Remmel J. B., and Scedrov A. Polynomially graded logic I: A graded version of system T. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 375\u2013395. IEEE Computer Society Press, 1989.","DOI":"10.1109\/LICS.1989.39192"},{"key":"3_CR54","doi-asserted-by":"publisher","first-page":"494","DOI":"10.2307\/2269958","volume":"36","author":"R. J. Parikh","year":"1971","unstructured":"Parikh R. J. Existence and feasibility in arithmetic, J. Symb. Logic, 36: 494\u2013508, 1971.","journal-title":"J. Symb. Logic"},{"key":"3_CR55","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1090\/S0002-9947-1973-0432416-X","volume":"177","author":"R. J. Parikh","year":"1973","unstructured":"Parikh R. J. Some results on the lengths of proofs, Trans. Amer. Math. Soc., 177: 29\u201336, 1973.","journal-title":"Trans. Amer. Math. Soc."},{"key":"3_CR56","volume-title":"Formal Logic","author":"A. N. Prior","year":"1962","unstructured":"Prior A. N. Formal Logic. Clarendon Press, Oxford, 1962."},{"key":"3_CR57","unstructured":"Proclus. A commentary on the first book of Euclid\u2019s Elements: Proclus, translated with introduction and notes by Glenn R. Morrow; [with a new foreword by Ian Mueller]. Princeton University Press, Princeton, NJ, 1970."},{"key":"3_CR58","volume-title":"The Autobiography of Bertrand Russell","author":"B. A. W. Russell","year":"1967","unstructured":"Russell B. A. W. The Autobiography of Bertrand Russell, 3 vols. Allen and Unwin, London, 1967\u20131969."},{"key":"3_CR59","first-page":"495","volume-title":"From Frege to G\u00f6del","author":"M. Sch\u00f6nfinkel","year":"1967","unstructured":"Sch\u00f6nfinkel M. Ueber die Bausteine der mathematischen Logik. In J. van Heijenoort, editor, From Frege to G\u00f6del, pages 495\u2013515. Harvard University Press, Cambridge, MA, 1967. Originally appeared in Mathematische Annalen, vol. 92, 305\u2013316, 1924."},{"key":"3_CR60","volume-title":"Beweistheorie","author":"K. Sch\u00fctte","year":"1960","unstructured":"Sch\u00fctte K. Beweistheorie, 1st ed. Springer, Berlin, 1960.","edition":"1"},{"volume-title":"The Collected Papers of Gerhard Gentzen","year":"1969","key":"3_CR61","unstructured":"Szabo M. E., editor. The Collected Papers of Gerhard Gentzen. North Holland Publishing Company, Amsterdam, 1969."},{"key":"3_CR62","doi-asserted-by":"publisher","first-page":"153","DOI":"10.2307\/2268280","volume":"2","author":"A. M. Turing","year":"1937","unstructured":"Turing A. M. Computability and lambda-definability, J. Symb. Logic, 2: 153\u2013163, 1937.","journal-title":"J. Symb. Logic"},{"key":"3_CR63","volume-title":"Principia Mathematica","author":"A. N. Whitehead","year":"1925","unstructured":"Whitehead A. N., and Russell B. A. W. Principia Mathematica, 3 vols. Cambridge University Press, Cambridge, 1925\u201327. first published in 1910\u201313."},{"key":"3_CR64","unstructured":"\u00c9s\u00e9nine-Volpine A. S. [Yesenin-Volpin]. Le programme ultra-intuitionniste des fondements des math\u00e9matiques. In Infinitistic methods, Proceedings of the Symposium on Foundations of Mathematics, Warsaw, 2\u20139 September 1959, pages 201\u2013223. Pergammon Press, Oxford; Pa\u0144stwowe Wydawnictwo Naukowe, Warszawa, 1960."}],"container-title":["Proof, Computation and Agency"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-94-007-0080-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,4]],"date-time":"2025-03-04T19:51:45Z","timestamp":1741117905000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-94-007-0080-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9789400700796","9789400700802"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-94-007-0080-2_3","relation":{},"subject":[],"published":{"date-parts":[[2011]]}}}