5 Propositions and Inference
For when I am presented with a false theorem, I do not need to examine
or even to know the demonstration, since I shall discover its falsity
a posteriori by means of an easy experiment, that is, by a
calculation, costing no more than paper and ink, which will show the
error no matter how small it is ...
And if someone would doubt my results, I should say to him: "Let us calculate, Sir," and thus by taking to pen and ink, we should soon settle the question.
- Gottfried Wilhelm Leibniz(1677)
This chapter considers a simple form of a knowledge base that is told facts about what is true in the world. An agent can use such a knowledge base, together with its observations, to determine what else must be true in the world. When an agent is queried about what is true given a knowledge base, it can answer the query without enumerating the possible worlds, or even generating any possible worlds. This chapter presents a number of reasoning formalisms that use propositions. They differ in what is being proved, what background knowledge must be provided, and how the observations that the agent receives online are handled.
