**Mail folder:**QED**Next message:**cal@aero.org: "Continuing Conversation - NO Flames"**Previous message:**John Harrison: "Formalizing notations and context"**Maybe in reply to:**John Harrison: "Formalizing notations and context"

Message-id: <wftm7jiKmlE2FjpoFQ@arp> Date: Wed, 5 May 1993 12:09:51 +1000 (EST) From: Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au> To: qed@mcs.anl.gov Subject: Re: Formalizing notations and context Sender: qed-owner Precedence: bulk

In "swan.cl.cam.:104680:930505012709"@cl.cam.ac.uk John.Harrison@cl.cam.ac.uk writes: > Rather, I see the principal difficulty as being the large amount of informal or > semi-formal context which is traditionally associated with notations. For > example, flicking through the first few pages of Matsumura: "Commutative ring > theory" we find: > [... examples of how mathematicians can get flippant about context and > notation ...] > If one hopes to make mathematicians used to ignoring lowbrow details like this > use QED, then considerable powers of persuasion are called for. If it can't be > done, then some very difficult AI problems have to be faced! I feel that this issue should become one of the subprojects of QED: to allow for the use of natural mathematical context-dependent notations and other means of expression, possibly definable by the users themselves. This, certainly is a difficult AI problem, but not an insurmountable one. Since amongst the aims of the project is to give mathematics to the "masses" and also to attract real mathematicians to QED - a humane and intelligent interface which would be capable of swallowing and understanding equivalents of: > "If f:A->B is a ring homomorphism and J is an ideal of B, then f (J) is an > ideal of A and we denote this by A /\ J; if A is a subring of B and f is the > inclusion map then this is the same as the usual set-theoretic notion of > intersection. In general this is not true, but confusion does not arise." would be most helpful. I see this as a gradual process. It might look quite insurmountable at present to build a reasoning system which would accept something like: "In general this is not true, but confusion does not arise". But it may be less difficult to implement initially something that at least makes a little step in that direction and then improve on it. For example, upon having received a phrase like that from the user, the system could ask the user to be somewhat more specific and provide a few more hints which would allow the system to apply a more precise meaning to various statements within this particular domain. There is a European Community project called MEDLAR (Mechanising Deduction for Logics of Practical Reasoning) whose aim is to build a system for selling cars. The system must be capable of outguessing and outsmarting the customer, and if need be, even of lying (the things logic is used for nowadays!) - building a system which can understand what the user really means on top of what the user merely says is not a hopeless undertaking. Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au, Automated Reasoning Program - CISR, and Plasma Theory Group - RSPhysS, The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601, Australia, fax: (Australia)-6-249-0747, tel: (Australia)-6-249-0158