From owner-qed Fri Aug 12 06:54:17 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id GAA01329 for qed-out; Fri, 12 Aug 1994 06:53:06 -0500 Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id GAA01316 for ; Fri, 12 Aug 1994 06:52:56 -0500 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 12 Aug 1994 12:52:42 +0100 To: qed@mcs.anl.gov Subject: Re: Accept Diversity Date: Fri, 12 Aug 94 12:52:31 +0100 From: Richard Boulton Message-ID: <"swan.cl.cam.:085270:940812115246"@cl.cam.ac.uk> Sender: owner-qed@mcs.anl.gov Precedence: bulk I support Peter Andrews' remarks to this mailing list. A few comments: > Each item in the library would consist of some > representation of a theorem and a proof for the theorem, along with > information which would specify precisely the formal language, > definitions and terminology, postulates (theory), lemmas, and proof > system which were used in stating and proving the theorem. > Any person or group could register a proof system (which would > include a formal language and a specification of how theorems and > proofs are to be represented) with the QED library. I see nothing in this to ensure that the formal system used is consistent. It is fine to leave the choice of whether or not to accept a formal system to a logician or degree-level mathematician, but it is unlikely that some other users (e.g., high school students?) would be able to make an informed decision about this. It might be a good idea, therefore, to have certified and uncertified formal systems. A certified system would have been approved by a group of experts to be a `trustworthy' or `widely-accepted' system. The tools made available to the general public for accessing the database might only allow theorems associated with certified systems to be used, or would at least give a very clear warning if the user tries to exploit a result in an uncertified system. > (Eventually there may be a need to avoid cluttering the library with > trivialities, or trivial variants of items already stored, but that is > a separate issue beyond the scope of this discussion.) It might be useful to allow references to standard text books, etc., to be stored with a proof, not only to assist the user, but it might also help in finding duplicates if tidying up of the library is ever required. Now for some suggestions: It seems to me that QED has to be distributed, not only in human effort, but also in terms of where the data is stored. Can we make use of the World Wide Web? One can envisage having a QED browser much like the HTML browsers used for hypertext. Maybe the existing browsers can be used? I envisage that anyone could make their proofs available on The Web without any authorisation, but to be included in the official QED library the proof would have to be registered at one of a small number of sites (one or two on each continent). The contributor might send a request for a proof to be included, specifying only the hyperlink. A program at the official site could then follow the link, check the proof, and if acceptable include the link in the index (or whatever) of the QED library. It would then inform the other official sites of the new entry. As usage grows the number of official sites might have to become quite large so as not to overload any one site with users accessing the library. So, how about we begin by developing a language/format for specifying proof systems and proofs? The subscribers to this list could then, if they wish, write programs to put theorems from their favourite prover into the QED format. There are bound to be many inadequacies with the first attempt at the format; testing it with the various proof systems and libraries of theorems already in use should iron-out a lot of them. We might then be in a position to write some library-accessing tools, having real data to test them on. If the idea seemed to be working the next stage would be to start building a real QED library. Having a standard interface format for theorem provers has applications outside of QED and is something that funding could probably be obtained for fairly easily. Richard Boulton University of Cambridge Computer Laboratory