A man-machine theorem-proving system

摘要

This paper describes a man-machine theorem-proving system at the University of Texas at Austin which has been used to prove a few theorems in general topology. The theorem (or subgoal) being proved is presented on the scope in its natural form so that the user can easily comprehend it and, by a series of interactive commands, can help with the proof when he desires. A feature called DETAIL is employed which allows the human to interact only when needed and only to the extent necessary for the proof.The program is built around a modified form of IMPLY, a natural-deduction-like theorem proving technique which has been described earlier.A few examples of proofs are given.