Machine math, clarification

• Mail folder: QED
• Next message: beeson@cats.UCSC.EDU: "Re: Why should a mathematician be interested in QED?"
• Previous message: chou@CS.UCLA.EDU: "Why should a mathematician be interested in QED?"
• Reply: Alan Bundy: "Re: Machine math, clarification"

From: beeson@cats.UCSC.EDU
Date: Wed, 21 Apr 93 09:07:26 -0700
Message-id: <9304211607.AA08993@si.ucsc.edu>
To: chou@CS.UCLA.EDU, qed@mcs.anl.gov
Subject: Machine math, clarification
Sender: qed-owner
Precedence: bulk

Clarification inspired by Bob Boyer's remark:  Machine Math MUST
be a formal language, with a precise syntax and semantics.  However,
it must be UNLIKE currently known formal languages in that it must 
NOT be repulsive to mathematicians.  This must be accomplished by 
making the syntax of Machine Math sufficiently similar to what 
mathematicians currently write in journals.    

I have a good deal of experience (seven years of programming) 
building a system that incorporates precise rules for calculus, algebra,
and trigonometry, with the aim of making the computer user-friendly
to students of those subjects, and in particular, of automatically
producing step-by-step solutions as an A+ student should.  I learned
that ordinary mathematics DOES have precise rules, even though those
rules require thousands of lines to express rather than dozens.  
I believe the same goes for ordinary informal proofs.   Machine 
Math must solve the following proportion:
    
        Machine Math                      Lisp or C
       ______________                    _____________
         "core logic"                     machine or assembly code


Some kind of "core logic"  (a minimal logical apparatus) is inevitable,
for implementations, just as machine code can't be avoided if you want
to run algorithms.