Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 21 Apr 1993 04:43:05 +0100 Received: by antares.mcs.anl.gov id AA04125 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 20 Apr 1993 22:29:15 -0500 Received: from arp.anu.edu.au by antares.mcs.anl.gov with SMTP id AA04117 (5.65c/IDA-1.4.4 for ); Tue, 20 Apr 1993 22:29:04 -0500 Received: by arp.anu.edu.au id AA23983 (5.65c/IDA-1.4.2.9 for qed@mcs.anl.gov); Wed, 21 Apr 1993 13:28:40 +1000 Received: from Messages.7.15.N.CUILIB.3.45.SNAP.NOT.LINKED.arp.anu.edu.au.sun4.41 via MS.5.6.arp.anu.edu.au.sun4_41; Wed, 21 Apr 1993 13:28:40 +1000 (EST) Message-Id: Date: Wed, 21 Apr 1993 13:28:40 +1000 (EST) From: Zdzislaw Meglicki To: qed@mcs.anl.gov Subject: Machine Math Sender: qed-owner@mcs.anl.gov 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