|Abstract||mathematicians for over 60 years. Amazingly, the Argonne team's automated theorem-proving program EQP took only 8 days to find a proof of it. Unfortunately, the proof found by EQP is quite complex and difficult to follow. Some of the steps of the EQP proof require highly complex and unintuitive substitution strategies. As a result, it is nearly impossible to reconstruct or verify the computer proof of the Robbins conjecture entirely by hand. This is where the unique symbolic capabilities of Mathematica 3 come in handy. With the help of Mathematica, it is relatively easy to work out and explain each step of the dense EQP proof in detail. In this paper, I use Mathematica to provide a detailed, step-by-step reconstruction of the highly complex EQP proof of the Robbins conjecture.|
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Only published papers are available at libraries|
Similar books and articles
Herbert A. Simon & Stuart A. Eisenstadt (1998). Human and Machine Interpretation of Expressions in Formal Systems. Synthese 116 (3):439-461.
N. Shankar (1994). Metamathematics, Machines, and Gödel's Proof. Cambridge University Press.
Carlo Cellucci (2008). Why Proof? What is a Proof? In Giovanna Corsi & Rossella Lupacchini (eds.), Deduction, Computation, Experiment. Exploring the Effectiveness of Proof, pp. 1-27. Springer.
Peter Aczel, Harold Simmons & S. S. Wainer (eds.) (1992). Proof Theory: A Selection of Papers From the Leeds Proof Theory Programme, 1990. Cambridge University Press.
Mark McEvoy (2008). The Epistemological Status of Computer-Assisted Proofs. Philosophia Mathematica 16 (3):374-387.
Peter Milne (2008). Russell's Completeness Proof. History and Philosophy of Logic 29 (1):31-62.
Liang Yu (2011). A New Proof of Friedman's Conjecture. Bulletin of Symbolic Logic 17 (3):455-461.
Added to index2009-01-28
Total downloads31 ( #44,754 of 722,698 )
Recent downloads (6 months)1 ( #60,006 of 722,698 )
How can I increase my downloads?