Publication Details

Application of Theorem Proving to Problem Solving

by Green, C.

Technical Note 4
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave, Menlo Park, CA 94025
Mar 1969.

Note: Project 7494
Presented at IJCAI 1969

Order an AIC Technical Note

Abstract

This paper shows how an extension of the resolution proof procedure can be used to construct problem solutions. The extended proof procedure can solve problems involving state transformations. The paper explores several alternate problem representations and provides a discussion of solutions to sample problems including the “Monkey and Bananas” puzzIe and the “Tower of Hanoi” puzzle. The paper exhibits solutions to the problems obtained by QA3, a computer program based on the theorem-proving methods. In addition, the paper shows how QA3 can write simple computer programs and can solve practical problems for a simple robot.

Electronic Copies

Adobe PDF

BibTeX

EndNote

Associated Projects

Research on Intelligent Automata A continuation of the original Shakey robot project, investigating AI problems involved in developing a robot.

AIC Personnel