Accession Number:

ADA459656

Title:

Application of Theorem Proving to Problem Solving

Descriptive Note:

Corporate Author:

SRI INTERNATIONAL MENLO PARK CA ARTIFICIAL INTELLIGENCE CENTER

Personal Author(s):

Report Date:

1969-03-01

Pagination or Media Count:

23.0

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 puzzle and the Tower of Hanoi puzzle. The paper exhibits solutions to these problems obtained by QA3, a computer program based on these theorem-proving methods. In addition, the paper shows how QA3 can write simple computer programs and can solve practical problems for a simple robot.

Subject Categories:

  • Computer Programming and Software
  • Cybernetics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE