The basic idea behind the use of logic (see Chapter 5) is that, when knowledge base designers have a particular world they want to characterize, they can select that world as an intended interpretation, select meanings for the symbols with respect to that interpretation, and write, as axioms, what is true in that world. When a system computes a logical consequence of a knowledge base, a user that knows the meanings of the symbols can interpret this answer with respect to the intended interpretation. Because the intended interpretation is a model, and a logical consequence is true in all models, a logical consequence must be true in the intended interpretation. This chapter expands the propositional logic to allow reasoning about individuals and relations. Atomic propositions now have internal structure in terms of relations and individuals.

The mapping between the symbols in the mind and the individuals and relations denoted by these symbols is called a conceptualization. This chapter assumes that the conceptualization is in the user’s head, or written informally, in comments. Making conceptualizations explicit is the role of a formal ontology.

What is the correct answer is defined independently of how it is computed. The correctness of a knowledge base is defined by the semantics, not by a particular algorithm for proving queries. As long as an inference algorithm is faithful to the semantics, it can be optimized for efficiency. This separation of meaning from computation lets an agent optimize performance while maintaining correctness.