Application of Theorem Proving to Problem Solving

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1969
Accession Number
ADA459656

Entities

People

  • Cordell Green

Organizations

  • SRI International

Tags

Communities of Interest

  • Autonomy

DTIC Thesaurus Topics

  • Artificial Intelligence
  • Automatic Programming
  • Computer Programming
  • Computer Programs
  • Computers
  • Construction
  • Databases
  • Debugging
  • Language
  • Pattern Recognition
  • Programming Languages
  • Recursive Functions
  • Semantics
  • Side Effects
  • Simulations
  • Systems Science

Fields of Study

  • Mathematics

Readers

  • Computational Linguistics
  • Finite Element Method (FEM) for solving Partial Differential Equations (PDEs)

Technology Areas

  • AI & ML
  • AI & ML - Machine Learning Algorithms
  • Autonomy