The Role of Formal Theorem Proving in Artificial Intelligence
by Raphael, Bertram
Technical Note 63
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave, Menlo Park, CA 94025
Feb 1972.
Note: First of two lecture to be presented at JITA (Japanese Industrial Technology Association) International Symposium on Information Processing Systems, Tokyo, March 6-17, 1972. SRI Projects 8776 and 1530. This lecture is based upon research supported at SRI by the National Science Foundation under Grant GJ-1060, and by the Advanced Research Projects Agency of the Department of Defense, monitored by U. S. Army Research Office-Durham under Contract DAHCO4 72 C 0008.
This tutorial paper begins by dividing Artificial Intelligence into three major subfields: formal problem solving, machines that understand, and machines that interact with the physical world. Each subfield contains a need for a component of formal logic. After summarizing the basic concepts of Mathematical Logic, the paper defines both the Propositional Calculus and the First-Order Predicate Calculus and describes some proof procedures for each. Finally, techniques are outlined for tailoring the Resolution proof method to particular kinds of problems of Artificial Intelligence.
 Adobe PDF |
 BibTeX |
 EndNote |
| Name | Title | ||
|---|---|---|---|
| Raphael, Bertram | Alumnus |
