Prolegomena to a Theory of Formal Reasoning
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
This paper is an introduction to the mechanization of a theory of reasoning. Currently formal systems are out of favor with the AI community. The aim of this paper is to explain how formal systems can be used in AI by explaining how traditional ideas of logic can be mechanized in a practical way. The paper presents several new ideas each of which is illustrated by giving simple examples of how it is mechanized in the reasoning system FOL. In this paper 1 we show how to mechanize the notion of model using the idea of simulation structure and explain why this is particularly important to AI 2 we show how to mechanize the notion of satisfaction 3 we present a very general evaluator for first order expressions, which subsumes PROLOG and which we propose as a natural way of thinking about logic programming 4 we show how to formalize metatheory 5 we describe reflection principles, which connect theories to their metatheories in a way new to AI 6 we show how these ideas can be used to dynamically extend the strength of FOL by 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 it own properties.
- Computer Programming and Software