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 what facts and rules hold 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 queried about what must be true given a knowledge base, it answers 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 observations are handled.