Delivery-Date:
From: Larry Wos <wos@mcs.anl.gov>
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@mcs.anl.gov
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