---
title: "A Man-Machine Theorem-Proving System"
authors:
  - "W. W. Bledsoe"
  - "Peter Bruell"
doi: ""
url: "https://ijcai.org/proceedings/1973/9"
pdf: "https://ijcai.org/proceedings/1973/0009.pdf"
venue: "Proceedings of the Third International Joint Conference on Artificial Intelligence"
year: 1973
pages: "56-65"
track: "Theorem Proving and Logic: 1"
keywords:
---

# A Man-Machine Theorem-Proving System

W. W. Bledsoe, Peter Bruell

*Proceedings of the Third International Joint Conference on Artificial Intelligence*, 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.