Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 22 Apr 1993 18:17:01 +0100 Received: by antares.mcs.anl.gov id AA23647 (5.65c/IDA-1.4.4 for qed-outgoing); Thu, 22 Apr 1993 12:08:21 -0500 Received: from sun2.nsfnet-relay.ac.uk by antares.mcs.anl.gov with SMTP id AA23640 (5.65c/IDA-1.4.4 for ); Thu, 22 Apr 1993 12:08:19 -0500 Via: uk.ac.edinburgh.aifh; Thu, 22 Apr 1993 15:54:00 +0100 Received: from etive.aisb.ed.ac.uk by aisb.ed.ac.uk; Thu, 22 Apr 93 09:54:11 BST Date: Thu, 22 Apr 93 09:54:10 BST Message-Id: <27363.9304220854@etive.aisb.ed.ac.uk> From: Alan Bundy Subject: Re: Machine math, clarification To: beeson@cats.ucsc.edu Phone: 44-31-650-2716 Fax: 44-31-650-6516 Cc: qed@mcs.anl.gov Sender: qed-owner@mcs.anl.gov Precedence: bulk > Clarification inspired by Bob Boyer's remark: Machine Math MUST > be a formal language, with a precise syntax and semantics. However, > it must be UNLIKE currently known formal languages in that it must > NOT be repulsive to mathematicians. This must be accomplished by > making the syntax of Machine Math sufficiently similar to what > mathematicians currently write in journals. I agree with the above remarks, but note that if taken literally the QED system would have to cope with remarks like "similarly", "proof trivial", "by symmetry", etc. Ultimately, it might be possible to cope with some proof descriptions containing such remarks by building tactics that can try to reproduce the proofs they imply. However, it will certainly be a non-trivial task. Alan Bundy