Donald Cohen

Knowledge Based Theorem Proving and Learning Degree Type: Ph.D. in Computer Science
Advisor(s): Scott Fahlman
Graduated: May 1980

Abstract:

This thesis argues that automatic deduction systems should keep large amounts of knowledge of many domains. This should include not only theorems (declarative knowledge) but diverse methods for solving different kinds of problems, programs to do forward reasoning and programs to transform one form of knowledge into another (all of which are forms of procedural knowledge). A program which does these things is presented. Major amounts of effort have gone into transforming theorems into other theorems which will be more useful, into forward inference programs, and into problem solving programs. The procedural knowledge, in turn, generates more declarative knowledge. A database is presented in which all of this knowledge can be stored so as to facilitate the retrievals that are desired. A goal tree is presented which enables the system to make use of its ability to disprove results, search for examples etc. as well as prove goals. This enables the system to understand, eg that proving one goal can cause another goal to be disproved. Also, several methods are presented which illustrate interesting uses for forward inference and communication between different parts of the database and the goal tree.