John Staples
During May 18-20 I participated in the QED Workshop at Argonne National
Laboratory, Illinois.
The purpose of the workshop was to progress the planning of the proposed
QED project. The aims of this project are outlined in the QED Manifesto,
available from me or by anonymous ftp from info.mcs.anl.gov:pub/qed/manifesto.
In brief, the proposal is to create a public-domain database of a
substantial part of mathematical knowledge, including proofs suitable for
machine checking.
Participants represented a wide range of theorem-proving projects:
- apologies for the inadequacies of the following list, which includes
only names of people, and of systems in which they have declared a current
interest as a developer or user; `*' indicates declared interest in proof
system development issues, but not declaration of a system name.
Michael Beeson (Mathpert)
Bob Boyer (Boyer-Moore theorem prover, also NQTHM)
Bernda Ingo Dahn (Proof Pad)
Masami Hagiya (*)
John Harrison (HOL)
Joan Hart (Otter)
M. Randall Holmes (*)
Paul Jackson (Nuprl)
Thomas Jech
Deepak Kapur (*)
Ken Kunen (Otter)
Ewing Lusk (*)
Bill McCune (Otter)
Chet Murthy (Coq)
Ross Overbeek
Bill Pase (Eves)
Piotr Rudnicki (Mizar)
John Staples (Qu-Prolog, Ergo)
Rick Stevens
F. Javier Thayer (Imps)
Andrzej Trybulec (Mizar)
Tomas Urbie (*)
Ralph Wachter
Richard Waldinger (*)
Toby Walsh (*)
Larry Wos (Otter, ...)
In view of the enormous scope of the project, it is important that it
be well-designed, both technically and so as to involve the large number
of people who will need to cooperate to ensure its success. This sort
of strategic planning is difficult and messy; the QED workshop was no
exception.
The workshop did not explicitly approve a list of recommendations. Rather,
reports such as this one are to be used as input to the process of
generating a report on the Workshop. Accordingly, I summarise below what
I think came out of the workshop.
(1) CORE REQUIREMENTS:
* A (single) metatheory.
Comment: This metatheory would formalise the coherence of the
whole project. It would define the scope and limits of the
object logics theories which could potentially be used, provide
a basis for defining and reasoning about relationships between
object theories, enable formal description of axiom schemes,
and so on.
* A database of formalised mathematics, including proofs (and their
contexts) which are amenable to mechanical checking.
Comment: The theories in the database would be QED object theories
(or, metalevel descriptions of them). There was a strong desire
to minimise the number of overlapping or competing theories in the
database (e.g. set theory vs higher order logic) but no clear idea
about how the political obstacles to that would be overcome.
* A mechanism for moderating database entries.
Comment: This mechanism would need to involve both human judgement
and appropriate tools such as proof checkers. The meeting did not
consider how the project would be administered, but that is
obviously crucial. Note the potential, given an appropriate
metatheory, for a single proof-checker to be developed which would
check proofs in *any* QED object theory, provided it is input a
metatheoretic description of the object theory whose proofs are
to be checked.
* Perhaps, for some object theories at least, an associated high-
level authoring language which authors of QED object theories
could use.
Comment: The Mizar project demonstrates that an authoring language
can encourage contributions from mathematicians by offering a
paradigm which is relatively close to writing proofs on paper.
It also provides a discipline for builders of automatic theorem
provers - check the gaps in the proofs of a relatively literate
authoring language. If authoring languages can focus the energies
of those communities then they are to be valued. It is not clear
however that they make the most of opportunities for interactive
support. Currently at least they seem to be rather batch-oriented.
(2) POTENTIAL USES FOR A QED DATABASE:
* Teaching and referencing mathematics.
Comment: `Referencing' covers a wide range of applications,
for example: encyclopaedic reference; a database for future
mathematical calculators; a database of reuseable information
for formal verification (e.g. of software and systems).
* Checking the accuracy of new mathematical proofs.
Comment: This seems to me a viable long-term goal, but in
setting up QED there's no benefit in adopting a `holier-than-thou'
attitude towards mathematicians.
* On-line archiving of formalised mathematics.
Comment: The isolation of current projects means that wheels are
often re-invented, and existing achievements are often lost.
(3) RESEARCH COMMUNITIES POTENTIALLY INTERESTED IN QED:
* Computer scientists, re: automated deduction; support for
developing verified systems; support for reuseable specifications
and designs.
* Mathematicians, re: a publication medium; a proof-checking resource;
a teaching and reference resource.
* Logicians, re: as for mathematicians; plus, this opens up a whole
new research area.
Comment: I imagine most people at the QED workshop would *not* want
QED to create a whole new research area for logicians! I don't
suggest QED needs to wait for new logical research. However I do
believe that as QED gains experience with supporting mathematics,
the benefit of formalising more of ordinary mathematical discourse
will become clear. For example, mathematical logic has so far
largely ignored the formalisations of:
* the bindings involved in definite and indefinite integral
notations;
* the introduction of such bindings as defined notation;
* proofs of correctness of such definition mechanisms.
For such reasons, QED should allow for long-term evolution of the
QED concept.
(4) POTENTIAL SIGNIFICANCE OF QED TO THE WIDER COMMUNITY:
* More attractive and productive mathematics teaching, leading to
increased mathematical literacy and higher average levels of
mathematical skill.
* More efficient professional use of mathematical reasoning, leading
to reduced costs and/or higher levels of quality assurance.
* Increased industrial reuse of mathematical reasoning, e.g. in
development of verified systems, leading to increased productivity.
Comment: I believe that clarifying the benefits of QED to the
wider community is the best approach to attracting the support of
mathematicians as well as the support of sponsors. I believe that
at this stage arguments that QED can benefit mathematics would
not be credible to most mathematicians.
(5) IMMEDIATE ACTIONS:
* Project-to-project discussions on sharing.
* Clarify the metatheory/metasystem proposal.
* Set up a problem database at Argonne to which can be contributed
benchmark examples of the use of various systems.
First example. Prove from the following axioms of group theory:
x(y.z) = (x.y).z
x.1 = x
x.i(x) = 1
the theorem
1.x = x
Comment: For this group theory problem, a deliberate decision was
made *not* to specify an informal proof. However the following
proof, adapted from p.4 of Hall's `The Theory of Groups' (Macmillan
1959) may be of assistance:
Step 1: show i(x).x = 1.
i(x).x = i(x).(x.1)
= (i(x).x).1
= (i(x).x).(i(x).i(i(x)))
= ((i(x).x).i(x)).i(i(x))
= ((i(x).(x.i(x))).i(i(x))
= (i(x).i(i.(x))
= 1
Step 2: show 1.x = x.
1.x = (x.i(x)).x
= x.(i(x).x)
= x.1
= x