BOUNCE qed@mcs.anl.gov: Admin request

owner-qed@mcs.anl.gov
Mon, 31 Oct 1994 06:31:11 -0600

>From lusk Mon Oct 31 06:31:06 1994
Received: from compu735.mathematik.hu-berlin.de (compu735.mathematik.hu-berlin.de [141.20.54.12]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id GAA10670 for <qed@mcs.anl.gov>; Mon, 31 Oct 1994 06:30:54 -0600
Received: from kummer.mathematik.hu-berlin.de by compu735.mathematik.hu-berlin.de with SMTP
(1.37.109.8/16.2/4.93/main) id AA22818; Mon, 31 Oct 1994 13:30:39 +0100
Received: from Helios.mathematik.hu-berlin.de by mathematik.hu-berlin.de (4.1/SMI-4.1/JG)
id AA20068; Mon, 31 Oct 94 13:30:47 +0100
Date: Mon, 31 Oct 94 13:30:47 +0100
From: dahn@mathematik.hu-berlin.de (Dahn)
Message-Id: <9410311230.AA20068@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: Re: Who are the intended customers of QED?

I'm a mathematician having experience with several provers and with other mathematicians. Therefore, I should give some comments to Chou's mail:

Mathematicians:
It is true that mathematicians (including logicians like me) are happy with informal proofs. But informal proofs can contain a lot of details and managing these details can be quite tedious. Mathematicians are willing to accept any help for this work and to pay for it. E. g. my university paid for a campus licence of Mathematica and it is used in our Institute of Pure Mathematics by mathematicians working in Differential Geometry. Mathematica is used to
- visualize objects
- perform formal algebraic operations,
- test examples.
The programming facilities of Mathematica are hardly used. From people working in numeric mathematics I know, that they use Mathematica to test conjectures, but they don't trust in it.

As Chou conjectures correctly, a main hurdle for using the more advanced features of Mathematica is the need to master a special language.

Theorem Provers:
As with the programming language of Mathematica, mathematicians certainly do not want to learn how to set the flags and parameters of a theorem prover. Therefore, provers are required that can set their switches automatically or have reasonable default settings. Even than the outcome can be frustrating. We use in ILF the following editor-like approach to hide the prover from the mathematical-minded user:
The user inserts lines of a proof and some provers in the background try to verify automatically, that the arguments given by the user are formally correct. If they are, the status of the lines is set automatically to >proved<. If not, then the user has to supply more detailed arguments. There is no need for the user to know anything about the calculi or the technology of the background provers.
Experiments show, that currently available provers can reduce the number of formulas that have to be typed in by the user to about 10%. Thus, the lines entered by the user look like an informal proof.
Certainly, provers should be just one aspect of creating a QED-environment for the work of mathematicians.

Other customers:
QED tools may find customers in other fields, where formal specifications have to be met, though the emphasis in these fields maybe more on establishing provability than in actual proofs. Mathematics is a particularly appropriate field to begin with because it has clear concepts and problems of very different complexity to test methods.

ID