%0 Report %@ 63 %A Raphael, Bertram %T The Role of Formal Theorem Proving in Artificial Intelligence %C 333 Ravenswood Ave, Menlo Park, CA 94025 %I AI Center, SRI International %D 1972 %K Artificial Intelligence, Problem Solving, Calculus, Formal Logic, Mathematical Logic %X 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. %O 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. %U http://www.ai.sri.com/pubs/files/1481.pdf

©2016 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493

SRI International is an independent, nonprofit corporation. Privacy policy

SRI International is an independent, nonprofit corporation. Privacy policy