A Man-Machine Theorem-Proving System

Bledsoe, W. W.; Bruell, Peter

A Man-Machine Theorem-Proving System

Download BibTeX Cite

Proceedings of the Third International Joint Conference on Artificial Intelligence. Theorem Proving and Logic: 1. Pages 56-65.

Abstract

This paper describes a man-machine theorem proving system at the University of Texas (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.

W. W. Bledsoe, and Peter Bruell. 1973. A Man-Machine Theorem-Proving System. In Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73. IJCAI, 56–65. https://ijcai.org/proceedings/1973/9

@inproceedings{ijcai1973p9,
  title     = {A Man-Machine Theorem-Proving System},
  author    = {Bledsoe, W. W. and Bruell, Peter},
  booktitle = {Proceedings of the Third International Joint Conference on
               Artificial Intelligence, {IJCAI-73}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Nils J. Nilsson},
  pages     = {56--65},
  year      = {1973},
  month     = {8},
  note      = {Theorem Proving and Logic: 1},
  url       = {https://ijcai.org/proceedings/1973/9},
}

TY  - CPAPER
TI  - A Man-Machine Theorem-Proving System
AU  - Bledsoe, W. W.
AU  - Bruell, Peter
T2  - Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1973
SP  - 56
EP  - 65
UR  - https://ijcai.org/proceedings/1973/9
ER  -