Delivery-Date:
Date: Tue, 25 Oct 94 15:54:21 +0100
From: dahn@mathematik.hu-berlin.de (Dahn)
Message-Id: <9410251454.AA04960@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: Bookkeeping
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

Javier writes:

> I agree that a central bookkeeping system might be useful to some
> individuals for some purposes. But I don't believe that it would
> necessarily encourage cooperation, especially if the bookkeeping
> mechanism is unwieldy.

I don't think that bookkeeping must be that complicated for the user. One of
the challenges of bookkeeping is to provide tools for managing proofs of
different systems and a uniform proof format. Of course, there should be tools
for the automatic conversion to the uniform format. This gives the possibility
to build complex proofs out of simple proofs even without translation into a
uniform calculus. This is apparently the only way to use results from other
groups.

Example: We have configured our system ILF to support editing of proofs from
the theory of lattice ordered groups. It integrated Otter, Setheo, Discount and
a domain specific prover Threelat. None of these systems would be as powerful
as their combination and the combination required bookkeeping of proofs from
different systems in different calculi.

Here, all proofs were produced within the same integrated system. But
bookkeeping will be of even greater importance, if proofs from other systems
are about to be used - not reproved for a specific purpose. (cf. the role of
references in MIZAR - however, unlike MIZAR, it would be desirable to have
access to a database of proofs, not just to their textual representation.)

Summing up: Bookkeeping - made easy for the user - can encourage cooperation
and exchange because everybody can participate in more advanced projects using
the books that others have written.

Ingo Dahn