The Syntactic Theory of Belief and Knowledge.

Artificial Intelligence programs must have common-sense knowledge. This includes knowledge about beliefs and knowledge. If we have a knowledge representation that can represent facts about beliefs and knowledge, and an adequate set of inference rules, we have taken the first step in building a program that can reason about beliefs and knowledge. The next step is to devise a search strategy an algorithm that decides which inference rules to apply to which expressions to solve a problem. This paper proposes a representation and inference rules for reasoning about belief and knowledge. The core of the paper is a series of examples of representation and inference in the formal system. These examples describe the processes that create, store and use beliefs and knowledge. Perception, introspection, memory, inference and planning are all considered. Finally there is an appendix with proofs that the formalism works as claimed.