Date: Wed, 23 Aug 95 09:05:57 +0200
From: dahn@mathematik.hu-berlin.de (Bernd Ingo Dahn)
Message-Id: <9508230705.AA20979@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: QED Framework
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

While the first QED workshop had put emphasis on the discussion of the 
basic understandings of the QED project, the second also gave a survey on 
existing expertise that can be used to bring QED into life. Moreover, there 
seemed to be sufficient consensus among the participants of the Warsaw 
workshop on goals that would be desirable to achieve in order to proceed.
Logically, the next step is to aim to concrete projects that push QED 
forward. These will be based on the state of the art that has become 
apparent in the 2nd QED workshop. It is widely agreed that QED is not a 
monolithic system but gives room to a variety of cooperating approaches. 
Therefore, I propose, that the QED community should actually use its 
scientific authority in order to support projects that promise progress 
towards the aims of QED. It is not important, that authors of such projects 
believe in the feasilbilty of QED. It is not even necessary, that their 
projects have computer aided mathematics as a principal goal. The only 
point to make is, that these projects yield results that are useful for 
QED.

To be more concrete, I propose to set up a description of topics and 
problems where research is especially encouraged. The intended readers of 
such a description are

- researchers looking for fields of application for their current work,
- researchers planning their future work or preparing proposals for 
projects,
- staff of institutions that consider funding of related projects,
- referees of  of related proposals and papers.

I would prefer, if this QED framework is not anonymous, but signed by many 
competent contributors where at least some of them offer to the readers 
further advice on request.

In order to launch a discussion I attach a list of topics that may be of 
importance for QED. Most of them have been touched at the 2nd QED Workshop. 
I am looking forward to comments to extend or modify this list. I expect to 
mail a revised version in October.


Ingo Dahn

***************************************
* Bernd, Ingo Dahn		      *
*				      *
* Humboldt-University		      *
* Institute of Pure Mathematics       *
* Ziegelstr. 13a		      *
* D-10099 Berlin		      *
*				      *
* Phone: (+49)30-2843-1829	      *
* Fax  : (+49)30-2843-1846            *
* Mail : dahn@mathematik.hu-berlin.de *
*				      *
***************************************


---------------------------------------------------------------------------

QED Framework						V. 1.1 (8/23/95)
=============

Projects in (at least) the following topics are valuable for the QED 
project and should be supported:


Proof Production
----------------

+ Automated theorem provers with special abilities. 
The production of formal proofs can benefit considerably from the support 
by automated theorem provers. While there are very refined universal 
theorem provers, little is known about the technology of provers which take 
advantage from domain specific properties, except for associativity and 
commutativity. Other relevant fields could be set inclusions, finite sets, 
finite and infinite sequences and number systems.
It is important, that the provers should be easy to combine with each other 
and with automated and interactive general purpose provers. This requires a 
welldefined input/output format, the possibility to accept limited 
resources and support for the selection of well-suited problems.

+ Tools that support the generation of formalized proofs based on standard 
mathematical texts.
A major problem for QED is the presentation of a large body of already 
existing proofs in a format that can be verified. Actual mathematical texts 
are mostly far from such a format. The tools should support the extraction 
of the verifiable part of  standard proof  texts. Moreover, they should 
supply their users with all available information that can be useful to 
complete the extracted proof skeleton 

+ Tools that support the generation and formalization of examples.
Examples play an important role in mathematics. Though most of them are not 
used in proofs, they are very useful for mathematicians in order to 
understand mathematical concepts. If the QED library is to be used by 
mathematicians, it is desirable that it also contains a selection of  
examples. Also the mathematical techniques to build new examples and to 
derive their properties should be supported. Methods to represent 
(infinite) models and to use them in automated and interactive proof search 
need further investigations.

+ Tools that facilitate the tuning of automated theorem provers.
The fruitful application of most current automated theorem provers requires 
solid knowledge of  their specific logical calculi and methods of proof 
search. This knowledge cannot be expected from a working mathematician. 
Therefore, provers should tune themselve to adapt to the problems they are 
supposed to solve. According to standard mathematical practice it can be 
assumed that a prover will be faced with a large sequence of problems from 
a specific domain. Alternatively, there may be mechanisms to detect a 
change of domain and a necessity of re-tuning.

+ Projects that aim to formalize or verify specific parts of mathematics.
Such projects yield the basis to test QED tools. Thus they will give 
valuable hints for further improvements. Moreover they give the basis to 
present the achievements to potential users. In order to extend the QED 
library as fast as possible, mathematical topics that have applications in 
many other fields of mathematics should be preferred. To support reuse of 
the results, the formalization should be in a precisely defined format 
which is easy to parse.


Proof Checking
--------------

+ Proof checkers for specific systems
These check the correctness of proofs in a specific calculus. The 
underlying calculus must be sound and should be complete with respect to a 
mathematically defined semantics. The format of the proofs to be checked 
must be precisely documented. If a proof is found to be incorrect or 
incomplete appropriate informations should be returned in a standardized 
format. The proof checking algorithm as well as its implementation have to 
be available to the public in an extensively documented format. Their 
correctness and completeness should be proved at least by standard 
mathematical tools. 

+ Generic proof checkers
These provide a language to specify proof concepts. Thus they can be used 
to check the correctness of proofs in several calculi.The general remarks 
made for proof checkers for specifiic systems also apply.

+ Proof translation between logical calculi
The aim is, to translate proofs in calculi without a proof checker into 
proofs in a calculus where a proof checker is available. Since the success 
of proof checking in the target calculus will guarantee the existence of a 
correct proof, the demands to formal verification of the transformation 
need not be as strict as for the proof checkers themselves.

Proof Administration and Exchange
---------------------------------

+ Tools for administring QED libraries
QED libraries will be large collections of formulas, definitions, theories 
examples and proofs. They can be distributed worldwide. The contents of 
these libraries has to be structured in an appropriate way. Besides the 
usual technology known from bibliographical databases specific retrieval 
tools will be helpful. These 
should tolerate slight logical or linguistic variants of formulas or 
theories. Search for incompletely specified formulas should be supprted. It 
must be possible to generate entries into the library automatically. The 
methods by which a theorem in the library has been verified will be 
documented. The  answers to search requests should be available in a format 
that can be easily parsed as well as in a human readable format.

+ Tools for the transformation of proofs and theories
It will be necessary to bring together proofs and theories from different 
sources and in different formats to make them available to different 
systems. Moreover, human users with differing interests and knowledge will 
use the QED libraries. Therefore, there is a need to adapt the material in 
the libraries to special purposes (calculi, systems, readers).


Proof Presentation
------------------

+ Input/Output-Tools for mathematicians
It should be possible for mathematicians with little extra knowledge to use 
and extend QED libraries.  The interface language should be as close to the 
usual language of mathematicians as possible.  There will be support for 
entering incomplete or partially verified proofs. The extent to which these 
are verified will be documented automatically and there will be support for 
the use of proof checkers.

+ Tools that integrate QED libraries into the existing world of 
mathematical 
education and research.
QED libraries should be made available to the mathematician at his desktop 
and in libraries. There should be methods to refer in mathematical 
publications to entries in QED libraries and vice versa.