Models and Entailment

Most of this site estimates quantities that are uncertain. This path asks a different question: given what a system already knows, what must be true? That question has a definite answer, and the machinery for computing it is logic.

Three definitions

A knowledge base (KB) is a set of sentences asserted to be true. A model is one complete assignment of truth values to every symbol - a fully specified possible world. Writing $M(\alpha)$ for the set of models in which $\alpha$ is true, the central relation is entailment:

$$\text{KB} \models \alpha \quad\text{iff}\quad M(\text{KB}) \subseteq M(\alpha).$$

In words: $\alpha$ holds in every model where the KB holds. Russell & Norvig's image is worth keeping. Think of the consequences of the KB as a haystack and $\alpha$ as a needle: entailment is the needle being in the haystack, inference is the procedure that finds it. The first is a fact about meaning; the second is an algorithm, and they can be discussed separately.

Deciding it by enumeration

Three squares may each hold a pit, so there are $2^3 = 8$ possible worlds. The KB says two things: there is no breeze at $[1,1]$, so its neighbour $[1,2]$ is clear; and there is a breeze at $[2,1]$, so at least one of $[2,2]$, $[3,1]$ holds a pit.

Three models survive. Now read conclusions off them:

• "no pit in $[1,2]$" is true in all three, so it is entailed;
• "no pit in $[2,2]$" is false in two of them, so it is not entailed;
• and neither is its negation, because it is true in the third.

Not entailing $\alpha$ is not entailing $\lnot\alpha$. Two of the three models put a pit in $[2,2]$ and one does not, so the evidence simply fails to settle that square. Reporting "no pit" or "pit" would both be claims the KB does not support - the honest answer is that it is undetermined.

Try it live. Enumerate the eight worlds and let the definition of entailment answer all three questions for you:

This procedure - enumerate every model, check that $\alpha$ holds wherever the KB does - is model checking, and it is a direct transcription of the definition.

All eight worlds are in the figure below, with the three that survive the knowledge base marked. Pick a conclusion and the table marks something more useful still: every surviving world in which that conclusion is false. For “no pit in [2,2]” there are two of them, and each one is a world entirely consistent with everything known - which is what “not entailed” means, and why asserting the opposite would be just as unsupported. Switch a sentence of the KB off and watch the surviving set grow.

Sound, complete, and expensive

Once inference is a procedure rather than a definition, two properties matter. A procedure is sound (Russell & Norvig also say truth-preserving) if everything it derives is genuinely entailed: it never announces the discovery of a needle that is not there. It is complete if it derives everything that is entailed: it never misses one.

Model checking is both - sound because it implements the definition, complete because it examines every model. The problem is cost: $n$ symbols give $2^n$ models, and Russell & Norvig record that propositional entailment is co-NP-complete, so exponential worst-case behaviour is intrinsic rather than a weakness of this particular algorithm. Our three symbols gave eight rows; thirty would give over a billion.

That is the motivation for the next lesson. A resolution prover does not enumerate worlds at all - it manipulates sentences syntactically, deriving conclusions with a single inference rule. What no practical reasoner does is build the whole table: DPLL-style SAT solvers do still search truth assignments, but one partial assignment at a time.

Before the quiz

Be able to state entailment as a subset relation between model sets, run a small enumeration and read off what it does and does not settle, define soundness and completeness separately, and say why model checking is exact yet impractical. The article Logic and Knowledge Representation covers the same ground at more length.