A Computer-Assisted Instruction Program for Exercises on Finding Axioms. Technical Report Number 186.

An interactive computer-assisted system for teaching elementary logic is described, which was designed to handle formalizations of first-order theories suitable for presentation in a computer-assisted instruction environment. The system provides tools with which the user can develop and then study a nonlogical axiomatic theory along whatever lines he specifies. These tools include a proof-checking program that allows the user to construct derivations by taking advantage of the theorem-proving capabilities of the computer. Results of preliminary investigations using this computer-assisted teaching system in a manner designed to give the student greater control over the organization of his curriculum are summarized, and initial studies on the uses of mechanical theorem provers in teaching about proof construction are outlined. (Author/RH)