Significant Contributions
Principia Mathematica was a milestone work in formal logic written by Alfred North Whitehead and Bertrand Russell. Principia Mathematica - also meaning Principles of Mathematics - was written with a purpose to derive all or some of the mathematical expressions, in terms of symbolic logic. Principia Mathematica was initially published in three volumes in 1910, 1912 and 1913.
Logic Theorist (LT) was the first ever program developed in 1956 by Allen Newell, Cliff Shaw and Herbert A. Simon to "mimic human reasoning" in proving theorems and was demonstrated on fifty-two theorems from chapter two of Principia Mathematica, proving thirty-eight of them. In addition to proving the theorems, the program found a proof for one of the theorems which was more elegant than the one provided by Whitehead and Russel. After an unsuccessful attempt at publishing their results Newell, Shaw and Herbert reported in their publication in 1958, The Next Advance in Operation Research:
-
- "There are now in the world machines that think, that learn and that create. Moreover, their ability to do these things is going to increase rapidly until (in a visible future) the range of problems they can handle will be co- extensive with the range to which the human mind has been applied."
Examples of Formal Proofs
-
Year Theorem Proof System Formalizer Traditional Proof 1986 First Incompleteness Boyer- Moore Shankar Godel 1990 Quadratic Reciprocity Boyer- Moore Russinoff Eisenstein 1996 Fundamental- of Calculus HOL Light Harrison Henstock 2000 Fundamental- of Algebra Mizar Milewski Brynski 2000 Fundamental- of Algebra Coq Geuvers et al. Kneser 2004 Four Color Coq Gonthier Robertson et al. 2004 Prime Number Isabelle Avigad et al. Selberg-Erdos 2005 Jordan Curve HOL Light Hales Thomassen 2005 Brouwer Fixed Point HOL Light Harrison Kuhn 2006 Flyspeck 1 Isabelle Bauer- Nipkow Hales 2007 Cauchy Residue HOL Light Harrison Classical 2008 Prime Number HOL Light Harrison analytic proof
Read more about this topic: Automated Reasoning
Famous quotes containing the word significant:
“Grandparents can be role models about areas that may not be significant to young children directly but that can teach them about patience and courage when we are ill, or handicapped by problems of aging. Our attitudes toward retirement, marriage, recreation, even our feelings about death and dying may make much more of an impression than we realize.”
—Eda Le Shan (20th century)