Re: Formalizing notations and context

Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>
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