reactions

• Mail folder: QED
• Next message: dts@dcs.ed.ac.uk: "Re: Cold water"
• Previous message: David McAllester: "Expansion Factors"

From: Larry Wos <wos>
Date: Mon, 26 Apr 93 12:28:32 CDT
Message-id: <9304261728.AA20030@altair.mcs.anl.gov>
To: qed@mcs.anl.gov
Subject: reactions
Sender: qed-owner
Precedence: bulk

 
Successes, Theorems, and proofs
 
  Here are some thoughts on topics found in the correspondence.
  
 To me, it is clear why mathematicians do care and will care more in the future.
If the community gets very, very good at proof checking, then progress of
a substantial nature will occur in proof finding.
The reason seems obvious:  When checking a proof, one is usually
given a proof with many gaps, gaps to be filled in by the system.
My recent experiments (with McCune's program OTTER)
in the context of proof checking have provided (for me)
ample evidence that gap filling is a tough problem to solve.
Since mathematics is vitally interested in proof finding, even though as yet the role of the computer
does not fascinate many, mathematicians will (when we get even better)
be interested in QED, at least indirectly.
 
 The additional impetus for their interest rests with a marvelous
database of theorems and definitions and proofs, which will be
one of the components of QED.
Anybody who has browsed in the library looking for some needed
lemma or theorem will feel glee at the thought of a good database of
mathematical information, including proofs.
  
  In my research, even at the beginning in 1963, I find the examination
of proofs and of failures to get proofs often leads to significant advances.
In that regard, and in partial answer to a recent question,
we maintain a database of input and output files, proofs, theorems, and
commentary, accessible by anonymous FTP.
We have proved theorems from group theory, ternary Boolean algebra, algebraic geometry,
topology, Tarskian geometry, and various logic calculi.
Indeed, with OTTER (and its predecessors), we have answered a number of open questions.
  
  As for the underlying logic, I cannot avoid my bias:
I am deeply committed to FOPC and, more specifically,
to the clause language.
I believe, without sufficient data, that the richer the language, the more difficult it is to control.
Since my interest is in proof finding, and since I am certain that
much strategy is required for attacking deep questions,
I vastly prefer the clause language:  It works better
than anything of which I know--sorry for the bias based on the group in which I work.
  
  More generally, I prefer set theory, and currently strongly
suspect that the various higher-order approaches offer far less
promise than does the FOPC approach.
  
  Extremely encouraging to me is the fact that mathematicians
such as I. J. Kaplansky as early as 1980 thought the activity
of automated reasoning important.
Currently, the reaction to a paper appearing in the January Notices
on automated reasoning (in Keith Devlin's column) has produced
a promising increase in interest.
Clearly, the New York Times article of say July 1991 is nonsense:
We can and do produce proofs of interest to mathematicians and
proofs that they can and d learn from.
  
  LW