Prolegomena to a Theory of Formal Reasoning
Richard W. Weyhrauch · 1978
This paper is an introduction to the mechanization of a theory of reasoning.Currently formal systems are out of favor with the Al community.The aim of this paper is to explain how formal Systems can be used in A ! by explaining how traditional ideas of logic can be mechanized in a practical way.The paper presents several new Ideas ~ Each of1these is illustrated by giving simple examples of how ~this ldea is mechanized in the reasoning system FOL. .\ That is, this is not just theory but there is an existing running implementation of these ideas.-) In this paper: ' 1) we show how to mechanize the notion of model using the idea of a simulation structure and explain why this Is particularly important to Al; 2) we show how to mechanize the notion of satisfactioni 3).we ptesent a very general evaluator for first order expressions, which subsumes P ~OLOG and we propose as a natural way of thinking about logic programming, 4) we show how to formalize metatheory, 5) we describe reftection principles, which connect theories to their metatheories in a way new to Al; (6) we show how these ideas can be used to dynamically extend the strength of FOL by 4 implementing' subsidiary deduction rules , and how this in turn can be extended to provide a method of describing and proving theorems about heuristics for using these rules ~ 7) we discuss one notion of what it could mean for a computer to learn and give an example, ~8) we describe a new kind of formal system that has the property that it can reason about Its ~vn properties .9) we give examples of all of the above.Sp onsored 1 ~ Me Advanced Researc h Projects Agency of the Department of Defense under ARPA Order No. 2494 , Contract MDA9O -76 .C.0206.The views and conclusions contained in this document are those of th.