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