{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:49:21Z","timestamp":1725558561947},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141270"},{"type":"electronic","value":"9783642141287"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_30","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T10:45:36Z","timestamp":1277808336000},"page":"345-354","source":"Crossref","is-referenced-by-count":1,"title":["Proofs, Proofs, Proofs, and Proofs"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Kerber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Abrams, P.S.: An APL machine. SLAC-114 UC-32 (MISC). Stanford University, Stanford, California (1970)","DOI":"10.2172\/4169175"},{"key":"30_CR2","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth through Proof","author":"P.B. Andrews","year":"1986","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press, Orlando (1986)"},{"key":"30_CR3","volume-title":"Language, Truth and Logic","author":"A.J. Ayer","year":"1936","unstructured":"Ayer, A.J.: Language, Truth and Logic, 2nd edn., 1951 edn. Victor Gollancz Ltd. London (1936)","edition":"2"},{"key":"30_CR4","unstructured":"Bourbaki, N.: Th\u00e9orie des ensembles. In: \u00c9l\u00e9ments de math\u00e9matique, Fascicule 1, Hermann, Paris, France (1954)"},{"key":"30_CR5","first-page":"579","volume-title":"To H.B.\u00a0Curry - Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"N.G. Bruijn de","year":"1980","unstructured":"de Bruijn, N.G.: A survey of the project Automath. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B.\u00a0Curry - Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 579\u2013606. Academic Press, London (1980)"},{"key":"30_CR6","first-page":"5","volume-title":"Handbook of Automated Reasoning","author":"M. Davis","year":"2001","unstructured":"Davis, M.: The early history of automated deduction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, pp. 5\u201314. Elsevier Science, Amsterdam (2001)"},{"key":"30_CR7","unstructured":"Frege, G.: Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle (1879)"},{"key":"30_CR8","unstructured":"Hales, T.: The Flyspek Project (2010), http:\/\/code.google.com\/flyspeck\/"},{"key":"30_CR9","unstructured":"Hardy, G.: A Mathematician\u2019s Apology. Cambridge University Press, London (1940)"},{"volume-title":"From Frege to G\u00f6del \u2013 A Source Book in Mathematical Logic, 1879-1931","year":"1967","key":"30_CR10","unstructured":"van Heijenoort, J. (ed.): From Frege to G\u00f6del \u2013 A Source Book in Mathematical Logic, 1879-1931. Harvard Univ. Press, Cambridge (1967)"},{"key":"30_CR11","volume-title":"Mathematical Reasoning with Diagrams: From Intuitions to Automation","author":"M. Jamnik","year":"2001","unstructured":"Jamnik, M.: Mathematical Reasoning with Diagrams: From Intuitions to Automation. CSLI Press, Stanford (2001)"},{"key":"30_CR12","volume-title":"Mathematics \u2013 The Loss of Certainty","author":"M. Kline","year":"1980","unstructured":"Kline, M.: Mathematics \u2013 The Loss of Certainty. Oxford University Press, New York (1980)"},{"key":"30_CR13","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139171472","volume-title":"Proofs and Refutations","author":"I. Lakatos","year":"1976","unstructured":"Lakatos, I.: Proofs and Refutations. Cambridge University Press, Cambridge (1976)"},{"key":"30_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569739","volume-title":"Fallacies in Mathematics","author":"E.A. Maxwell","year":"1959","unstructured":"Maxwell, E.A.: Fallacies in Mathematics. Cambridge University Press, Cambridge (1959)"},{"issue":"3","key":"30_CR15","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problems. Journal of Automated Reasoning\u00a019(3), 263\u2013276 (1997), http:\/\/www.mcs.anl.gov\/home\/mccune\/ar\/robbins\/","journal-title":"Journal of Automated Reasoning"},{"key":"30_CR16","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Selected Papers on Automath","year":"1994","unstructured":"Nederpelt, R., Geuvers, H., de Vrijer, R. (eds.): Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics, vol.\u00a0133. North-Holland, Amsterdam (1994)"},{"key":"30_CR17","unstructured":"Nederpelt, R., Kamareddine, F.: An abstract syntax for a formal language of mathematics. In: The Fourth International Tbilisi Symposium on Language, Logic and Computation (2001), http:\/\/www.cedar-forest.org\/forest\/papers\/conference-publications\/tbilisi01.ps"},{"key":"30_CR18","volume-title":"Mathematics and Plausible Reasoning","author":"G. P\u00f3lya","year":"1954","unstructured":"P\u00f3lya, G.: Mathematics and Plausible Reasoning. Princeton University Press, Princeton (1954); Two volumes, Vol. 1: Induction and Analogy in Mathematics, Vol. 2: Patterns of Plausible Inference"},{"key":"30_CR19","volume-title":"Natural Deduction \u2013 A Proof Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"Prawitz, D.: Natural Deduction \u2013 A Proof Theoretical Study. Almqvist & Wiksell, Stockholm (1965)"},{"key":"30_CR20","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5680.001.0001","volume-title":"The Psychology of Proof \u2013 Deductive Reasoning in Human Thinking","author":"L.J. Rips","year":"1994","unstructured":"Rips, L.J.: The Psychology of Proof \u2013 Deductive Reasoning in Human Thinking. The MIT Press, Cambridge (1994)"},{"key":"30_CR21","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine oriented logic based on the resolution principle. Journal of the ACM\u00a012, 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"30_CR22","unstructured":"Trybulec, A.: The Mizar logic information language. In: Studies in Logic, Grammar and Rhetoric, Bia\u0142ystok, Poland, vol.\u00a01 (1980)"},{"key":"30_CR23","volume-title":"Principia Mathematica","author":"A.N. Whitehead","year":"1910","unstructured":"Whitehead, A.N., Russell, B.: Principia Mathematica, vol.\u00a0I. Cambridge University Press, Cambridge (1910)"},{"key":"30_CR24","unstructured":"Wittgenstein, L.: Bemerkungen \u00fcber die Grundlagen der Mathematik. In: Suhrkamp-Taschenbuch Wissenschaft, 3rd edn., Frankfurt, Germany, vol.\u00a0506 (1989)"},{"key":"30_CR25","unstructured":"Claus Zinn. Understanding Informal Mathematical Discourse. PhD thesis, Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg, Erlangen, Germany (2004)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14128-7_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,6]],"date-time":"2020-06-06T06:47:54Z","timestamp":1591426074000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}