This report summarizes two years of research effort that included studies of computer memory organization, formal theorem-proving techniques, the application of theorem-proving techniques to new problem domains, and the use of limited natural language input to a question-answering system. The principal accomplishments of the project were
(a) the discovery of some interesting ways of relating formal theorem-proving to practical question-answering and problem-solving tasks, and
(b) the implementation of a system of computer programs that demonstrate the approach and facilitate further research.
This report describes briefly the areas of research covered, and then presents abstracts of four papers that contain extensive description and technical detail of the work.
SRI Project 6001