**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