From lusk Fri May 27 16:34:44 1994 Received: from scapa.cs.ualberta.ca (scapa.cs.ualberta.ca [129.128.4.44]) by antares10.mcs.anl.gov (8.6.4/8.6.4) with SMTP id QAA08892 for ; Fri, 27 May 1994 16:31:56 -0500 Received: from sedalia.cs.ualberta.ca by scapa.cs.ualberta.ca id <18547-1>; Fri, 27 May 1994 15:31:47 -0600 Subject: The workshop ended a week ago From: Piotr Rudnicki To: qed@mcs.anl.gov Date: Fri, 27 May 1994 15:31:39 -0600 X-Mailer: ELM [version 2.4 PL23] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 1208 Message-Id: <94May27.153147-0600.18547-1@scapa.cs.ualberta.ca> Hi: 1. Most of A. Trybulec's effort in Mizar has been on the systematic reconstruction of the language of mathematics as used among the mathematicians. This process is still in progress with no end in sight. If we are ever to involve the mathematicians in the QED effort we should have in mind that the the interface language to QED must be close to the language of the working mathematician. Mizar is still some distance away from this language, thoufh it can be closer than other proof-checking systems. I have a difficulty realising how the discussion on PRA or other root logic relates to this issue. 2. During the workshop we tried to answer the question: Who are consumers of QED? I do not remember much of this, and I do not have any notes. Does anybody have? My vision of QED consumers is kind of fuzzy mainly due to the following. I do not see that I can interest a working first-class mathematician in QED before QED includes most of, say, high-school mathematics. And now I have to come up with a scheme by which I get the high-school mathematics into QED data base. Does anybody has an idea of how to do it? -- Piotr (Peter) Rudnicki