A Man-Machine Theorem-Proving System
Abstract
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.
Cite
Text
Bledsoe and Bruell. "A Man-Machine Theorem-Proving System." International Joint Conference on Artificial Intelligence, 1973. doi:10.1016/0004-3702(74)90009-5Markdown
[Bledsoe and Bruell. "A Man-Machine Theorem-Proving System." International Joint Conference on Artificial Intelligence, 1973.](https://mlanthology.org/ijcai/1973/bledsoe1973ijcai-man/) doi:10.1016/0004-3702(74)90009-5BibTeX
@inproceedings{bledsoe1973ijcai-man,
title = {{A Man-Machine Theorem-Proving System}},
author = {Bledsoe, W. W. and Bruell, Peter},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1973},
pages = {56-66},
doi = {10.1016/0004-3702(74)90009-5},
url = {https://mlanthology.org/ijcai/1973/bledsoe1973ijcai-man/}
}