Delivery-Date: 
Message-Id: <9407121314.AA15044@easynet.crl.dec.com>
Date: Tue, 12 Jul 94 09:14:03 EDT
From: "Tim Leonard, DTN 225-5809, HLO2-3/C11 12-Jul-1994 0912" 
      <leonard@ricks.enet.dec.com> 
To: qed@mcs.anl.gov
Apparently-To: qed@mcs.anl.gov
Subject: What objects will QED work with? How? What's the UI?
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

As I understand it, QED is to:

  + provide computer-assisted trustworthy reasoning in all (or most, or many)
    areas of mathematics
  + support the apparently direct use of the theories and logics used in each
    area of math (rather than making users aware of a translation into one or
    more other logics)
  + use foundations and reasoning methods acceptable to almost all
    mathematicians and logicians
  + provide a user interface at least as good as provided by the best current
    math tools, like Mathematica and Maple

and QED is to be used by:

  + scientists, engineers, and others who apply mathematics and logic in their
    work, because QED will support the necessary mathematics, and will make new
    kinds of work possible or old kinds easier, and will provide trustworthy
    results
  + mathematicians, for exploration and discovery, because QED will support the
    mathematics of interest, and QED's automation will make new kinds of work
    possible, or old kinds easier (automated proof checking probably won't be
    a big selling point)
  + theorem prover builders, as a system to extend, learn from, steal from, and
    argue about

It seems to me that these issues need to be resolved before QED will really get
anywhere:

 1. How is the project to be funded, staffed, managed?
 2. What is to be the metalogic?
 3. What sorts of object-level objects are to be included, and how are those
    objects to be stored, maintained, generated, and interrelated?
 4. How are other provers' objects to be related/exported/imported to QED?
 5. What is the initial user interface to be?

The first two topics seem to have made some progress.  I'd like to see more
discussion of the others.

 3. What sorts of object-level objects are to be included, and how are those
    objects to be stored, maintained, and interrelated?

Potential sorts of objects include axioms, primitive inference rules, derived
rules, proofs, theorems, theories, syntactic objects and rules, names of
objects, other documentation of objects, and other relationships between
objects.  Are inference rules to be explicitly represented in an object-level
logic, so metalogical reasoning can be applied to them?  How will reflection be
implemented? Will it be possible to determine what axioms and rules a theorem
or theory depends on?  Will it be possible for a theorem or theory to have
several distinct bases of support?  Will it be possible for each of two
theories to provide a base of support for the other?  Will it be possible to
group alternative formulations of the same theorem, or theory?  Will a theorem
with several formulations, or with several bases of support, be "the same"
theorem or different theorems? 

 4. How are other provers' objects to be related/exported/imported to QED?

Is it a goal to exactly represent the logics used by other provers?  The
inference rules?  The proof scripts?  Is it a goal to automatically translate
to or from other provers' worlds?  Is it a goal to replace any other provers
or math tools, or only to supplement them?  Will QED interact with other
provers to produce proofs?  Will it be possible to label QED theorems or other
objects as the results of other provers? 

 5. What is the initial user interface to be?

What existing tools have the best user interfaces?  What makes them best?
What are their problems?  Will a QED user need to be a programmer?  Will a user
need to understand proof methods?  Can a few users be identified and recruited
to act as representatives of their kinds?  Can example problems be posed and
fake interactions be scripted to show what QED should someday be able to do?


In the hope of provoking some of that discussion, I'll volunteer some of my
opinions:

QED will need a rich world of object types, and a real database in which to
store them and their interrelationships.  Everything from syntax rules to
human-readable theorem descriptions should be in the database and accessible to
reasoning and search.  It should be possible to revoke an assertion and
everything that depends on it.  It should be possible to have many versions of
an object like a theorem.  It should be possible for set theory to act as the
base of support for a theory of functions, and for a theory of functions to act
as a support for set theory, without the need for two set theories and two
theories of functions (though it will require two sets of proofs).  It should
be possible to extract a theorem or theory together with its base of support. 

QED should try to replace several provers and math tools.  For example, QED
should try to be good enough to completely supercede Macsyma, HOL, nqthm,
Otter, and a good BDD-based prover.  QED should include exact representations
of the logics of those provers, and should support automatic translation of
proof scripts. (For HOL, that will entail automatic translation of SML code
into something QED can reason with.)