Abstract
In logic there is a clear concept of what constitutes a proof and what not. A proof is essentially defined as a finite sequence of formulae which are either axioms or derived by proof rules from formulae earlier in the sequence. Sociologically, however, it is more difficult to say what should constitute a proof and what not. In this paper we will look at different forms of proofs and try to clarify the concept of proof in the wider meaning of the term. This has implications on how proofs should be represented formally.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrams, P.S.: An APL machine. SLAC-114 UC-32 (MISC). Stanford University, Stanford, California (1970)
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press, Orlando (1986)
Ayer, A.J.: Language, Truth and Logic, 2nd edn., 1951 edn. Victor Gollancz Ltd. London (1936)
Bourbaki, N.: Théorie des ensembles. In: Éléments de mathématique, Fascicule 1, Hermann, Paris, France (1954)
de Bruijn, N.G.: A survey of the project Automath. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry - Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 579–606. Academic Press, London (1980)
Davis, M.: The early history of automated deduction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 5–14. Elsevier Science, Amsterdam (2001)
Frege, G.: Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle (1879)
Hales, T.: The Flyspek Project (2010), http://code.google.com/flyspeck/
Hardy, G.: A Mathematician’s Apology. Cambridge University Press, London (1940)
van Heijenoort, J. (ed.): From Frege to Gödel – A Source Book in Mathematical Logic, 1879-1931. Harvard Univ. Press, Cambridge (1967)
Jamnik, M.: Mathematical Reasoning with Diagrams: From Intuitions to Automation. CSLI Press, Stanford (2001)
Kline, M.: Mathematics – The Loss of Certainty. Oxford University Press, New York (1980)
Lakatos, I.: Proofs and Refutations. Cambridge University Press, Cambridge (1976)
Maxwell, E.A.: Fallacies in Mathematics. Cambridge University Press, Cambridge (1959)
McCune, W.: Solution of the Robbins problems. Journal of Automated Reasoning 19(3), 263–276 (1997), http://www.mcs.anl.gov/home/mccune/ar/robbins/
Nederpelt, R., Geuvers, H., de Vrijer, R. (eds.): Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics, vol. 133. North-Holland, Amsterdam (1994)
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
Pólya, 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
Prawitz, D.: Natural Deduction – A Proof Theoretical Study. Almqvist & Wiksell, Stockholm (1965)
Rips, L.J.: The Psychology of Proof – Deductive Reasoning in Human Thinking. The MIT Press, Cambridge (1994)
Robinson, J.A.: A machine oriented logic based on the resolution principle. Journal of the ACM 12, 23–41 (1965)
Trybulec, A.: The Mizar logic information language. In: Studies in Logic, Grammar and Rhetoric, Białystok, Poland, vol. 1 (1980)
Whitehead, A.N., Russell, B.: Principia Mathematica, vol. I. Cambridge University Press, Cambridge (1910)
Wittgenstein, L.: Bemerkungen über die Grundlagen der Mathematik. In: Suhrkamp-Taschenbuch Wissenschaft, 3rd edn., Frankfurt, Germany, vol. 506 (1989)
Claus Zinn. Understanding Informal Mathematical Discourse. PhD thesis, Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen, Germany (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kerber, M. (2010). Proofs, Proofs, Proofs, and Proofs. In: Autexier, S., et al. Intelligent Computer Mathematics. CICM 2010. Lecture Notes in Computer Science(), vol 6167. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14128-7_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-14128-7_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14127-0
Online ISBN: 978-3-642-14128-7
eBook Packages: Computer ScienceComputer Science (R0)