Machine Math

Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>

Mail folder: QED
Next message: chou@CS.UCLA.EDU: "Why should a mathematician be interested in QED?"
Previous message: beeson@cats.UCSC.EDU: "Machine Math"
Maybe in reply to: beeson@cats.UCSC.EDU: "Machine Math"
Reply: Dewey Val Schorre: "Re:Machine Math"

Message-id: <Ifp=xc6KmlE2FPg19g@arp>
Date: Wed, 21 Apr 1993 13:28:40 +1000 (EST)
From: Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>
To: qed@mcs.anl.gov
Subject: Machine Math
Sender: qed-owner
Precedence: bulk

In <9304202024.AA20321@si.ucsc.edu> beeson@cats.UCSC.EDU writes:

> I suggest the following organization of the QED effort:

> 1.  Machine Math language design and specification.
> 2.  Formalization of a sizeable body of mathematics in Machine Math.
> 3.  Specification of low-order logic(s) as target language(s).
> 4.  Construction of Machine Math compiler(s) into the target language(s).
> 5.  Construction of proof-checkers for the target languages.
> 6.  Construction of database software to manipulate a large body of 
>     mathematics in Machine Math form.        

Why can't proof-checking itself be also carried out in Machine Math. If
the language is sufficiently precise to allow formulation of theorems
and proofs by  human users it should be also sufficiently precise for
the machine to carry out reasoning in it.  "Mathematica" which has been
quoted in this context, has its own high level language in which
reasoning can be expressed and carried out. In other words, why not to
replace points 3, 4, and 5 with a direct translation from Machine Math
to machine code?

   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