From lusk Wed Jun 15 00:24:10 1994 Received: from uqcspe.cs.uq.oz.au (uqcspe.cs.uq.oz.au [130.102.192.8]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id AAA23516; Wed, 15 Jun 1994 00:22:04 -0500 Received: from everest.cs.uq.oz.au by uqcspe.cs.uq.oz.au id ; Wed, 15 Jun 94 15:21:24 +1000 Received: by everest (5.0/SMI-SVR4) id AA17930; Wed, 15 Jun 1994 15:21:21 --1000 Date: Wed, 15 Jun 1994 15:21:20 +1000 (EST) From: John Staples Subject: Report on QED Workshop To: qed@mcs.anl.gov, pieper@mcs.anl.gov Cc: staples@cs.uq.oz.au Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Content-Length: 7539 Report on QED Workshop 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