Dahn (
Tue, 25 Oct 94 15:54:21 +0100

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