**Mail folder:**QED**Next message:**Zdzislaw Meglicki: "Re: Incentive to write proofs"**Previous message:**Dewey Val Schorre: "Document -- What's Done and What's to be Done"**Maybe in reply to:**jt@linus.mitre.org: "Boyer's hypothesis"**Reply:**John Harrison: "Re: Boyer's Hypothesis"

Message-id: <0fqnwnqKmlE2MUS1dr@arp> Date: Mon, 26 Apr 1993 11:47:31 +1000 (EST) From: Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au> To: qed@mcs.anl.gov Subject: Re: Boyer's Hypothesis Sender: qed-owner Precedence: bulk

In <9304251444.AA06798@malabar.mitre.org> jt@linus.mitre.org writes: > If it turns out that the Boyer constant for proofs in these areas [i.e., > "real life" mathematics done in the last 30 years] is 10000, then much > of what we are talking about in this forum about "doing real > mathematics" is highly speculative and may border on self-deception. But, this is exactly where systems such as "Analytica" by E. Clarke and X. Zhao (CMU-CS-92-117) come in. The reason why "real life" mathematical proofs are so short is because they are not carried out all the way down to the logical foundations. Instead, they utilize already accumulated knowledge and prove things by reducing them to other already proven theorems. The pyramid of structures that has been built in this way over the last couple of hundred years is very high indeed, but this is also the most efficient way of doing things: "seeing further by standing on the shoulders of the giants". The QED system will have to incorporate somehow this way of doing things if it is at all to be workable and useful. In the "Analytica" report you'll find examples of various theorems from mathematical analysis and their mechanically constructed proofs - the culmination of the paper is a mechanical proof of Weierstrass' example of a continuous nowhere differentiable function. The proofs delivered by the system are short, quite comparable to similar proofs that would be produced by humans and perfectly readable. So the Boyer constant is *not* 10,000 in this case: it is about 1. It was possible to achieve that because the prover was built on the basis of a symbolic computation system for manipulating mathematical formulas already equipped in a very formidable data base of mathematical knowledge. What QED could add to a system like that would be a sound logical foundation. I.e., every one of the facts stored in its equally formidable data base would itself be a theorem with an accompanying proof. Although the proofs should not go all the way down to the underlying logic - rather, they should try to reduce problems to already proven theorems, the way it is done in man-made mathematics - by combining proofs of theorems on lower levels it should ultimately be possible to reconstruct mechanically the whole proof tree with its leaves at the level of the basic logic (although I am not sure why anybody would ever want to do that - apart from just demonstrating that it can be done). Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au, Automated Reasoning Program - CISR, and Plasma Theory Group - RSPhysS, The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601, Australia, fax: (Australia)-6-249-0747, tel: (Australia)-6-249-0158