Re: Machine math, clarification

Alan Bundy <bundy@aisb.ed.ac.uk>

Mail folder: QED
Next message: Robert S. Boyer: "Red Herring?"
Previous message: Tobias.Nipkow@informatik.tu-muenchen.de: "Root Logics"
In-reply-to: beeson@cats.UCSC.EDU: "Machine math, clarification"

Via: uk.ac.edinburgh.aifh; Thu, 22 Apr 1993 15:54:00 +0100
Date: Thu, 22 Apr 93 09:54:10 BST
Message-id: <27363.9304220854@etive.aisb.ed.ac.uk>
From: Alan Bundy <bundy@aisb.ed.ac.uk>
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
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