Re: How many false theorems are there?
yodaiken@chelm.cs.umass.edu (victor yodaiken)
Date: Mon, 5 Jul 1993 22:57:14 -0400
From: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Message-id: <9307060257.AA03113@chelm.cs.umass.edu>
To: LYBRHED@delphi.com, qed@mcs.anl.gov
Subject: Re: How many false theorems are there?
Sender: qed-owner
Precedence: bulk
I think that it's a mistake to consider automated deduction as a correction
to mathematical practice, much as such thoughts boost the egos of computer
scientists. IMHO automated deduction should aim at making it possible to
treat deduction as calculation. The "theorems" that we wish to prove
in computer science and engineering are quite different from the theorems
that traditionally interest mathematicians. We need to prove that a specific
piece of code computes a specific function or that there are no paths
between two nodes of a specific and very large graph that contain less
than a certain number of transitions, or that IEEE floating point calculations
given as a certain mathematical expression approximate the real valued
computation of that expression within some epsilon .... Proofs of these
low theorems are going to be long, complicated and far less likely to
be pretty or illuminating than proofs of the high theorems of
mathematics. It has been shown that some very complex applied algebra
and analysis can be automated to a degree (in MAPLE,Mathematica etc).
What we need to do is show that complicated and boring proofs can also
be automated.