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.