Logic and Knowledge Representation
Reasoning about what must be true: models and entailment worked by exhaustive enumeration, soundness and completeness, why propositional logic runs out of expressive power, and where first-order logic picks up.
Most of this site is about learning from data - estimating quantities that are uncertain, and being careful about how uncertain they are. There is an older tradition in artificial intelligence that asks a different question: given what I already know, what must be true?
That is not a statistical question. It admits a definite answer, and the machinery for computing it is logic.
A. Knowledge bases, models, entailment
A knowledge base (KB) is a set of sentences asserted to be true about the world. A model is one complete assignment of truth values to every proposition - one possible world, fully specified. A sentence is true in some models and false in others, and we write for the set of models in which is true.
The central relation is entailment:
- read "KB entails " - means is true in every model in which KB is true. Equivalently, .
The idea is familiar from arithmetic, where entails : in any world where is zero, is zero too, whatever happens to be.
Entailment is a fact about meaning, not about any algorithm. Russell & Norvig put the distinction memorably: think of the consequences of KB as a haystack and as a needle. Entailment is the needle being in the haystack; inference is finding it.
B. Working an entailment out by hand
Take the standard setting. An agent is exploring a grid of caves, some containing pits. A square is breezy exactly when an adjacent square contains a pit. The agent starts at , feels no breeze, moves to , and feels a breeze.
Three squares are in question: , , and . Each either holds a pit or does not, so there are possible worlds.
The KB says two things:
- No breeze at . Its neighbours are and , so neither holds a pit. In particular is pit-free.
- A breeze at . Its neighbours are , and . The agent stood safely in , so at least one of , holds a pit.
Enumerate all eight and mark where the KB holds:
| KB true? | |||
|---|---|---|---|
| - | - | - | no |
| - | - | pit | yes |
| - | pit | - | yes |
| - | pit | pit | yes |
| pit | - | - | no |
| pit | - | pit | no |
| pit | pit | - | no |
| pit | pit | pit | no |
Exactly three models survive. Now test two candidate conclusions.
: "there is no pit in ." True in all three surviving models. So - the agent may safely move there.
: "there is no pit in ." False in two of the three. So . Note carefully what this does not say: it does not establish that there is a pit in either, since one surviving model has none. The honest conclusion is that the evidence does not settle it.
Runs in your browser. The first run downloads the Python runtime (~10 MB), then it is cached.
This procedure - enumerate every model, check that holds wherever KB does - is model checking, and it is a direct transcription of the definition of entailment.
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.
Interactive: eight worlds, and the one that refutes you
Pick a conclusion. The table marks every world that survives the KB and denies it.
| [1,2] | [2,2] | [3,1] | KB true? | α true? |
|---|---|---|---|---|
| pit | pit | pit | no | no |
| pit | pit | - | no | no |
| pit | - | pit | no | yes |
| pit | - | - | no | yes |
| - | pit | pit | yes | no |
| - | pit | - | yes | no |
| - | - | pit | yes | yes |
| - | - | - | no | yes |
- Possible worlds
- 8
- Models of the KB
- 3
- Worlds refuting α
- 2
- Verdict
- undetermined
The knowledge base
The conclusion α
2 of the 3 surviving worlds deny α, and the rest support it, so the KB does not entail α - and it does not entail its negation either. The evidence simply fails to settle the square. Reporting either answer would be a claim the knowledge base does not support, and the marked rows are the proof: each one is a world entirely consistent with everything known, in which the conclusion is false.
C. Soundness, completeness, and cost
Once inference is a procedure rather than a definition, two properties matter. An algorithm is sound (or truth-preserving) if everything it derives is genuinely entailed: it never invents conclusions. It is complete if it can derive everything that is entailed: it never misses one.
Model checking is both. It is sound because it implements the definition directly, and complete because there are only finitely many models and it examines all of them.
The cost is the problem. With proposition symbols there are models, so the time complexity is - the space complexity is only , since the enumeration can be done depth-first. Our three unknowns gave eight rows; thirty would give over a billion.
Nor is this merely a weakness of one naive algorithm. Deciding propositional entailment is co-NP-complete, so no known method avoids exponential behaviour in the worst case. Practical systems therefore use inference rules that derive conclusions syntactically rather than enumerating worlds - Modus Ponens and its relatives - which are dramatically faster on typical problems while remaining sound.
Below is one of those relatives at work: a resolution prover, with its working shown, on a smaller knowledge base than the one above. It holds the rule that is breezy exactly when or has a pit, , and the percept , with no percept at . The clause list is that knowledge base converted to clauses, plus the negated query, and every line under it is a resolvent in the order the search produced it. Ask for "no pit at [1,2]" and the empty box appears; ask for "a pit at [1,2]" and the search saturates without it, which is an answer rather than a failure. Each query is also decided a second time by enumerating the eight worlds, with no code shared between the two, and the figure reports whether they agree.
Interactive: a refutation, clause by clause
Answered twice: by resolution, and by enumerating the eight worlds.
Knowledge base in CNF, with the negated query last
- !B11 v P12 v P21
- !P12 v B11
- !P21 v B11
- !B11
- P12
- Clauses to start
- 5
- New clauses derived
- 5
- Empty clause
- yes
- Model checking agrees
- yes
Resolvents, in the order the prover found them
- !P12 v B11 + !B11 -> !P12
- !P21 v B11 + !B11 -> !P21
- !P12 v B11 + P12 -> B11
- !B11 v P12 v P21 + !P12 -> !B11 v P21
- P12 + !P12 -> []
The empty clause appeared after 5 new clauses, and an empty disjunction is false in every model. So the knowledge base together with the negated query cannot be satisfied, which is precisely what it means for the knowledge base to entail the query. Model checking, enumerating all eight worlds and sharing no code with any of this, agrees.
D. Where propositional logic runs out
Everything above used propositions: atomic facts that are simply true or false. That is a genuine limitation, and it shows up as soon as you try to say something general.
To express "all squares adjacent to a pit are breezy" propositionally, you must write one sentence per square, and rewrite them all if the grid changes size. The rule itself - the thing you actually know - cannot be stated. Russell & Norvig's verdict is blunt: propositional logic is too puny a language to represent knowledge of complex environments concisely.
The difference is one of ontological commitment - what a language assumes about the nature of reality:
| Logic | Commits to |
|---|---|
| Propositional | Facts that hold or do not hold |
| First-order | Objects, and relations among them that hold or do not hold |
| Temporal | Facts holding at particular, ordered times |
| Higher-order | Relations and functions as objects in their own right |
First-order logic assumes the world contains objects with relations between them. That buys quantifiers - ("for all") and ("there exists") - and with them, generality. The breeze rule becomes a single sentence quantified over all squares, true regardless of how large the grid is.
Inference lifts accordingly. Generalized Modus Ponens applies the familiar rule to sentences containing variables by first finding a substitution that makes the premises match - a process called unification - and then applying to the conclusion. Reasoning that had to be repeated per object is done once, schematically.
That is an algorithm, so the figure below runs it: argument by argument, with each binding recorded as it is made, and both terms printed with the unifier applied so that "identical" can be read rather than asserted. Two failing pairs sit beside it. The occurs check is the one worth pressing - unifying x with Mother(x) has no solution, and an implementation that omits the check builds an infinite term instead of saying so.
Interactive: the most general unifier, computed
Argument by argument, with every binding recorded as it is made.
- Knows(John, x)
- Knows(y, Mother(y))
What the algorithm did, in order
- Knows(John, x) ~ Knows(y, Mother(y)) -> same symbol: match 2 arguments
- y ~ John -> bind y/John
- x ~ Mother(John) -> bind x/Mother(John)
- Unifiable
- yes
- Substitution
- {y/John, x/Mother(John)}
- Bindings made
- 2
- Both terms, unified
- Knows(John, Mother(John))
The unifier is {y/John, x/Mother(John)}, and applying it makes the two expressions the same string - which is what unification means rather than a claim about it. Notice how little it commits to: the substitution is the MOST GENERAL one, binding only what the match forces. A unifier that also bound some unrelated variable would work here and rule out instances a later step of the proof might need.
E. Why this still matters
It would be easy to file this as history. That would be a mistake, for three reasons.
Some knowledge is not statistical. Constraints, rules, definitions, and policies are naturally stated as sentences that hold or fail, and learning them from examples when you could simply write them down is wasteful and unreliable.
Logical conclusions come with guarantees. A sound inference procedure never returns a wrong answer, and it can show its work as a chain of applied rules. A learned model offers a probability and, usually, no derivation. Where correctness must be certified rather than estimated, that difference is decisive.
The representational question did not go away. How to encode what a system knows so that it can be combined and reasoned over is the same question whether the contents are hand-written axioms or extracted from a corpus. Ontologies, knowledge graphs, typed schemas, and constraint solvers are all descendants of this line of work.
The realistic position is that the two traditions answer different questions. Learning handles perception and uncertainty; logic handles structure and guaranteed consequence. Systems that need both tend to end up with both.
Key takeaways
- A knowledge base is asserted sentences; a model is one fully specified possible world.
- means holds in every model where KB holds - .
- Entailment is a semantic fact; inference is the search for it - needle and haystack.
- In the worked example, 8 possible worlds reduced to 3 consistent with the percepts, entailing "no pit in " but leaving genuinely undetermined.
- Failing to entail is not entailing .
- Sound means never wrong; complete means never missing. Model checking is both, at time and space.
- Propositional entailment is co-NP-complete, so worst-case exponential cost is intrinsic, not an artefact of a naive algorithm.
- Propositional logic cannot state general rules; first-order logic commits to objects and relations, gaining quantifiers and lifted inference.
What's next
For the probabilistic counterpart - reasoning when facts are not simply true or false but hold with some degree of belief - see Bayes' Theorem and Belief Updating, and for the decision-making layer built on top of it, Markov Decision Processes.
References & further reading
- Stuart Russell, Peter Norvig, Artificial Intelligence: A Modern Approach, Pearson (3rd edition), 2010· Kudos AI reference library
Copyrighted works are cited for reference only and are not hosted here; please consult the publisher for access.