Handing in Math Homework
By Richard Weyhrauch

This note is called: [MATH-HOMEWORK]
The notations used in this note is described in [NOTATION]
Under development

This note describes how the features of the original FOL system grew out of my goal to build a system that could read and print proofs as it might encounter in the homework assignments in a math course and then use the output to hand in the assignment and get it graded. The goa; was first to simply have a hman type in the assignment questiuons and their answers (a homework assistent). It did no0t have to solve the homework problem (theorem proving was to come later),\it simplyu had to accept the problem and be told the answer.

I started by implementing a system that could be told a first order language and would accept 'axioms' amd could make deductions if given the premises nd told what rule to apply. the structure of the program was like the LCF program of Robin Milnor except that it understood first order expressions and used natural deduction as described by Prawitzs. SAIL keyboard PCHECK