Re: Analytica and Boyer's Hypothesis
jt@linus.mitre.org
Message-id: <9304260309.AA07147@malabar.mitre.org>
To: qed@mcs.anl.gov
Subject: Re: Analytica and Boyer's Hypothesis
Date: Sun, 25 Apr 93 23:09:09 -0400
From: jt@linus.mitre.org
Sender: qed-owner
Precedence: bulk
--------
Zdzislaw Meglicki gives Analytica as an example of a theorem prover
which cooks up proofs having Boyer constant 1. For example, in his
contribution he states:
...the culmination of the paper is a mechanical proof of Weierstrass'
example of a continuous nowhere differentiable function.
But in my view his remarks fail to address my concern about the Boyer
constant for more recent mathematics. For example could one do Hans
Lewy's famous example of a PDE without a local solution, an example
dating from the mid-1950's, via a reasonable Boyer number? (Forget
about anything fancy, like figuring out when local solutions exist!)
Moreover, some of the strength of Analytica relies on its use of
algorithms it gets from Mathematica (eg. Gosper's algorithm, algebraic
simplification etc). This is not meant to in any way belittle the
importance of the work of Clarke and Zhao. Quite the contrary, the
fact Analytica uses algorithms of this kind, is in my view, an
intelligent design decision which has provided us with a great deal of
useful empirical evidence. However, one should be very cautious of
building a general purpose theorem prover on top of a system such as
Mathematica, which has an enormous number of documented "misfeatures."
I repeat my concern voiced earlier that we need to carefully
understand more proofs with a view to determining (or estimating) their
Boyer number.
Javier Thayer