---
title: Logical Agents and Propositional Logic
module: Logic and Planning
moduleNumber: 3
lessonNumber: 1
order: 301
summary: >
  A knowledge-based agent keeps a store of sentences and acts by asking it what
  to do. To make "asking" mean something we need entailment — the relation
  $KB \models \alpha$ that holds when every model of the knowledge base is a model
  of the query. Propositional logic gives a syntax and a truth-table semantics for
  which entailment is decidable. This first part builds the foundations: the
  agent loop, the Wumpus World, models and entailment, the connectives and truth
  tables, theorem proving by refutation, and the resolution rule with its CNF
  conversion — a single complete inference procedure for all of propositional logic.
topics: [Logic]
sources:
  - book: AIMA
    ref: "Ch. 7 — Logical Agents; §7.1 Knowledge-Based Agents; §7.2 The Wumpus World; §7.3 Logic"
  - book: AIMA
    ref: "§7.4 Propositional Logic; §7.5 Propositional Theorem Proving"
---

The [search agents](/artificial-intelligence/foundations/intelligent-agents) of
the previous module know things, but only in a thin, inflexible sense. The
transition model for a puzzle is buried inside the code of a successor function:
it can predict the outcome of an action, but it cannot _deduce_ that two tiles
never share a square, or that a goal is unreachable from where it stands. A **knowledge-based agent**
takes the opposite stance. It carries an explicit store of sentences about the
world, adds to that store as it perceives, and chooses actions by _reasoning_
over it — deriving new facts from old.[^aima-intro] The payoff is that the same
machinery accepts new goals as sentences, absorbs new information by being told,
and adapts to a changed world by updating what it believes, all without rewriting
the agent.

## The knowledge base and the agent loop

The central component is the **knowledge base**, or $KB$: a set of **sentences**,
each written in a **knowledge representation language** and each asserting
something about the world. A sentence taken as given, not derived from others, is
an **axiom**. Two operations act on the store. `Tell` adds a sentence; `Ask`
queries what follows from what is already there. Both may involve **inference** —
deriving new sentences from old — subject to a single requirement: when the agent
`Ask`s a question, the answer must
_follow_ from what has been `Tell`ed.

$$
% caption: A knowledge-based agent. Each cycle it tells the KB its percept, asks
% the KB which action to take, tells the KB the action it chose, and executes it;
% the reasoning that answers the query lives entirely inside Ask.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  box/.style={draw, minimum width=26mm, minimum height=11mm, align=center},
  kb/.style={draw, thick, minimum width=30mm, minimum height=26mm, align=center}]
  \definecolor{acc}{HTML}{2348F2}
  \node[box] (perc) at (0,1.6)  {percept};
  \node[box] (act)  at (0,-1.6) {action};
  \node[kb, draw=acc, text=acc] (kb) at (5.6,0) {knowledge\\base};
  \draw[->, acc, thick] (perc.east) to[out=0, in=140] node[above, font=\footnotesize, black] {\texttt{Tell}} (kb.150);
  \draw[->, acc, thick] (kb.210) to[out=220, in=0] node[below, font=\footnotesize, black] {\texttt{Ask}} (act.east);
  \node[font=\scriptsize, align=center] at (5.6,-2.15) {the reasoning\\is in here};
\end{tikzpicture}
$$

Each time the agent program runs, it does three things: it `Tell`s the $KB$ what
it just perceived; it `Ask`s the $KB$ what action to take, a query whose answer
may require extensive reasoning about the current state and the outcomes of action
sequences; and it `Tell`s the $KB$ which action it chose, before executing it.
Written out, the loop is short — the intelligence is hidden inside `Ask`.

```algorithm
caption: $\textsc{KB-Agent}$ — act by telling and asking a knowledge base
input: $percept$, the current percept
persistent: $KB$, a knowledge base; $t$, a counter, initially $0$
$\textsc{Tell}(KB, \textsc{Make-Percept-Sentence}(percept, t))$
$action \gets \textsc{Ask}(KB, \textsc{Make-Action-Query}(t))$
$\textsc{Tell}(KB, \textsc{Make-Action-Sentence}(action, t))$
$t \gets t + 1$
return $action$
```

Because `Tell` and `Ask` are defined by entailment, not by arbitrary code, the
agent admits a description at the **knowledge level**: we can say what it knows
and what its goals are, and predict its behavior, without knowing how the
knowledge is stored or manipulated at the **implementation level**. An automated
taxi that knows the only route to Marin crosses a particular bridge _because it
knows that will achieve its goal_ — an account that holds whether the knowledge
is a linked list, a pixel map, or a net of neurons. Building such an agent can be
as simple as `Tell`ing it, one sentence at a time, what it needs to know; this is
the **declarative** approach to system building, in contrast to the
**procedural** approach that hard-codes behavior directly.

## The Wumpus World

The **Wumpus World** is an environment where knowing things pays off: a cave of
rooms on a $4 \times 4$
grid, connected by passages. Somewhere in the cave lurks the wumpus, a beast that
eats anyone who enters its room; some rooms hold bottomless pits; and one room
holds a heap of gold. The agent starts in square $[1,1]$ facing right, can move
`Forward`, `TurnLeft`, or `TurnRight`, can `Grab` gold in its square, can `Shoot`
its single arrow in a straight line, and can `Climb` out from $[1,1]$. It dies
entering a pit or a live wumpus's room; the goal is to fetch the gold and climb
out alive.[^aima-wumpus]

The agent never sees the whole board. It gets five one-bit percepts: a **stench**
in the wumpus's square and the four directly adjacent to it; a **breeze** in any
square adjacent to a pit; a **glitter** in the square with the gold; a **bump**
on walking into a wall; and a **scream**, heard everywhere, when the wumpus dies.
From this local, indirect evidence the agent must infer a global map of hazards.

$$
% caption: A typical Wumpus World. The agent (A) starts in the bottom-left corner
% facing right. Breezes mark squares adjacent to a pit; a stench marks squares
% adjacent to the wumpus (W); the gold (G) lies in [2,3].
\begin{tikzpicture}[>=stealth, font=\footnotesize, scale=1.25,
  cell/.style={draw, fill=black!12, minimum size=5mm, inner sep=0pt, font=\scriptsize},
  lbl/.style={font=\tiny, red}]
  \definecolor{acc}{HTML}{2348F2}
  \definecolor{red}{HTML}{C0392B}
  % 4x4 grid
  \foreach \i in {0,...,4} \draw[black] (\i,0) -- (\i,4);
  \foreach \j in {0,...,4} \draw[black] (0,\j) -- (4,\j);
  % column / row indices
  \foreach \i/\lab in {0/1,1/2,2/3,3/4} \node[font=\scriptsize, black] at (\i+0.5,-0.3) {\lab};
  \foreach \j/\lab in {0/1,1/2,2/3,3/4} \node[font=\scriptsize, black] at (-0.3,\j+0.5) {\lab};
  % helper: cell (col c, row r) has centre at (c-0.5, r-0.5)
  % pits at [3,1],[3,3],[4,4]
  \foreach \c/\r in {3/1, 3/3, 4/4} \node[cell] at (\c-0.5,\r-0.5) {PIT};
  % breezes (adjacent to pits): [2,1],[4,1],[3,2],[2,3],[4,3],[3,4]
  \node[lbl] at (1.5,0.28) {Breeze};   % [2,1]
  \node[lbl] at (3.5,0.28) {Breeze};   % [4,1]
  \node[lbl] at (2.5,1.28) {Breeze};   % [3,2]
  \node[lbl] at (3.5,2.28) {Breeze};   % [4,3]
  \node[lbl] at (2.5,3.28) {Breeze};   % [3,4]
  % wumpus at [1,3]
  \node[draw=red, thick, fill=red!10, minimum size=5mm, inner sep=0pt, font=\scriptsize] at (0.5,2.5) {W};
  % stench (adjacent to wumpus): [1,2],[1,4],[2,3]
  \node[lbl] at (0.5,1.72) {Stench};   % [1,2]
  \node[lbl] at (0.5,3.72) {Stench};   % [1,4]
  % crowded cell [2,3]: stench (top), gold (middle), breeze (bottom), stacked
  \node[lbl] at (1.5,2.78) {Stench};
  \node[font=\tiny, acc] at (1.5,2.5) {Gold};
  \node[lbl] at (1.5,2.22) {Breeze};
  % agent at [1,1]
  \node[draw=acc, thick, fill=acc!10, minimum size=5mm, inner sep=0pt, font=\scriptsize] at (0.5,0.5) {A};
  \node[font=\tiny, acc] at (0.5,0.22) {start};
\end{tikzpicture}
$$

Trace the agent's reasoning from the start square. Its initial $KB$ holds the
rules of the game, so it knows $[1,1]$ is safe. The first percept is all-`None` —
no breeze, no stench — so neither neighbor $[1,2]$ nor $[2,1]$ hides a pit or
wumpus; both are OK. It steps to $[2,1]$ and now feels a breeze, so _some_
neighbor holds a pit; the pit cannot be in the visited-safe $[1,1]$, so it is in
$[2,2]$ or $[3,1]$ (or both) — a possibility, not a fact about either one. Rather
than gamble, the prudent agent returns and tries $[1,2]$, where it perceives a
stench. The wumpus is nearby, but not in $[1,1]$ (safe) and not in $[2,2]$
(else the earlier stop at $[2,1]$ would have smelled it): the wumpus must be in
$[1,3]$. And the _absence_ of a breeze in $[1,2]$ means $[2,2]$ has no pit, which
combined with the earlier deduction forces the pit into $[3,1]$. That last step
is genuinely hard — it fuses evidence gathered at different times in different
squares, and it turns on a percept that _did not_ occur. Every such conclusion,
when drawn from correct information, is guaranteed correct. That guarantee is the
whole point of logical reasoning, and the rest of this lesson makes it precise.

## Logic: models and entailment

Every logic rests on two ideas. Its **syntax** specifies which strings of symbols
are well-formed sentences — in ordinary arithmetic, "$x + y = 4$" is well formed
and "$x4y+ =$" is not.[^aima-logic] Its **semantics** defines the **truth** of
each sentence with respect to each **possible world**. When we want to be precise
we drop "possible world" for **model**: a model is a mathematical object that
fixes the truth or falsehood of every relevant sentence. If sentence $\alpha$ is
true in model $m$, we say $m$ **satisfies** $\alpha$, or $m$ is a model of
$\alpha$, and we write $M(\alpha)$ for the set of all models of $\alpha$.

That much semantics is enough to define reasoning. **Entailment** is the relation
that holds when one sentence follows logically from another. We write
$\alpha \models \beta$ to mean $\alpha$ **entails** $\beta$, and the definition is

$$
\alpha \models \beta \quad\text{if and only if}\quad M(\alpha) \subseteq M(\beta).
$$

In words: $\alpha \models \beta$ exactly when, in every model where $\alpha$ is
true, $\beta$ is true as well.[^aima-entail] Note the direction of the
$\subseteq$: if $\alpha \models \beta$ then $\alpha$ is the _stronger_ assertion,
because it rules out _more_ worlds. The relation is familiar from arithmetic —
$x = 0$ entails $xy = 0$, since in any world where $x$ is zero, $xy$ is zero too,
whatever $y$ is.

> **Definition (Entailment).** $\alpha \models \beta$ holds iff every model of
> $\alpha$ is a model of $\beta$, i.e. $M(\alpha) \subseteq M(\beta)$. A stronger
> sentence has fewer models and entails more; the always-false sentence entails
> everything, the always-true sentence is entailed by everything.

Apply this to the agent's reasoning after it has felt nothing in $[1,1]$ and a
breeze in $[2,1]$. Those percepts plus the rules form the $KB$. Ask whether the
three adjacent squares $[1,2]$, $[2,2]$, $[3,1]$ contain pits. Each may or may
not, so there are $2^3 = 8$ candidate models. The $KB$ is false in any model that
contradicts what the agent knows — false wherever $[1,2]$ has a pit, since then
$[1,1]$ would be breezy. Exactly three of the eight models satisfy the $KB$. Now
test two conclusions: $\alpha_1 = $ "no pit in $[1,2]$" and $\alpha_2 = $ "no pit
in $[2,2]$".

$$
% caption: The models of pit-placement, drawn as dots. The solid region is
% $M(KB)$, holding the three models of the knowledge base. It sits entirely inside
% $M(\alpha_1)$ (no pit in [1,2]), so $KB \models \alpha_1$. It is not inside
% $M(\alpha_2)$ (no pit in [2,2]): one KB-model (the one where [2,2] has a pit)
% falls outside, so $KB \not\models \alpha_2$.
\begin{tikzpicture}[>=stealth, font=\footnotesize]
  \definecolor{acc}{HTML}{2348F2}
  \definecolor{red}{HTML}{C0392B}
  % outer dashed region: M(alpha_1)
  \draw[dashed, acc, thick] (0,0) ellipse (5.0 and 2.6);
  \node[font=\scriptsize, acc, anchor=east] at (4.95,2.1) {models where a1 holds};
  % solid region: M(KB), three dots
  \draw[thick, black] (-2.7,0) ellipse (1.5 and 1.35);
  \node[font=\scriptsize, anchor=south] at (-2.7,1.4) {models of KB};
  \fill[black] (-3.2,0.45) circle (2.6pt);
  \fill[black] (-2.35,0.55) circle (2.6pt);
  \fill[black] (-2.7,-0.55) circle (2.6pt) coordinate (kbout);
  % dashed region: M(alpha_2) -- a lobe that covers 2 of the 3 KB dots but not the bottom one
  \draw[dashed, red, thick] (-2.75,0.55) ellipse (1.05 and 0.75);
  \node[font=\scriptsize, red, anchor=south west] at (-2.0,1.0) {a2 holds};
  % a few more models outside KB but inside alpha_1
  \foreach \x/\y in {0.6/0.9, 1.7/-0.6, 2.9/0.7, 0.2/-1.0} \fill[black] (\x,\y) circle (2.6pt);
  % annotate the KB-model that escapes alpha_2
  \node[font=\scriptsize, red, anchor=north] at (-2.7,-1.55) {KB-model with a pit in [2,2]};
  \draw[red, thick, ->] (-2.7,-1.35) -- (kbout);
\end{tikzpicture}
$$

Naming the three unknown squares $[1,2]$, $[2,2]$, $[3,1]$ and their pit variables
$p_{12}, p_{22}, p_{31}$, the eight candidate models are the eight rows of a truth
table. The percepts force $\lnot B_{1,1}$ (so $[1,2]$ and $[2,1]$ are pit-free by
$R_2$) and $B_{2,1}$ (so at least one of $[2,2]$, $[3,1]$ has a pit by $R_3$). Only
three rows survive: the ones with $p_{12} = \mathit{false}$ and $(p_{22} \lor
p_{31})$ true.

| $p_{12}$ | $p_{22}$ | $p_{31}$ | $KB$? | $\alpha_1{=}\lnot p_{12}$ | $\alpha_2{=}\lnot p_{22}$ |
| --- | --- | --- | --- | --- | --- |
| F | F | T | **T** | T | T |
| F | T | F | **T** | T | F |
| F | T | T | **T** | T | F |
| F | F | F | F | — | — |
| T | * | * | F | — | — |

Reading the three bold $KB$-rows: $\alpha_1$ is true in all three, so $KB \models
\alpha_1$; but $\alpha_2$ is false in two of them, so $KB \not\models \alpha_2$.

$$
% caption: The three surviving models of the wumpus $KB$, as rows of pit
% assignments to $[1,2],[2,2],[3,1]$. All three agree that $[1,2]$ is pit-free
% (so $\alpha_1$ is entailed); they disagree on $[2,2]$ (so $\alpha_2$ is not).
% The shaded row is the model where $[2,2]$ holds a pit — the one that escapes
% $\alpha_2$.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  hd/.style={font=\scriptsize\bfseries, text=black},
  c/.style={font=\scriptsize}]
  \definecolor{acc}{HTML}{2348F2}
  \definecolor{red}{HTML}{C0392B}
  \definecolor{tintr}{HTML}{F7E1DD}
  \node[hd] at (0,2.2)   {[1,2]};
  \node[hd] at (1.1,2.2) {[2,2]};
  \node[hd] at (2.2,2.2) {[3,1]};
  \node[hd] at (3.7,2.2) {a1 holds};
  \node[hd] at (5.4,2.2) {a2 holds};
  \draw[black] (-0.5,2.0) -- (6.2,2.0);
  % row 1
  \node[c] at (0,1.5) {no}; \node[c] at (1.1,1.5) {no}; \node[c] at (2.2,1.5) {PIT};
  \node[c, acc] at (3.7,1.5) {yes}; \node[c, acc] at (5.4,1.5) {yes};
  % row 2 (shaded: pit in [2,2], escapes a2)
  \fill[tintr] (-0.5,0.65) rectangle (6.2,1.15);
  \node[c] at (0,0.9) {no}; \node[c] at (1.1,0.9) {PIT}; \node[c] at (2.2,0.9) {no};
  \node[c, acc] at (3.7,0.9) {yes}; \node[c, red] at (5.4,0.9) {no};
  % row 3
  \node[c] at (0,0.3) {no}; \node[c] at (1.1,0.3) {PIT}; \node[c] at (2.2,0.3) {PIT};
  \node[c, acc] at (3.7,0.3) {yes}; \node[c, red] at (5.4,0.3) {no};
  \draw[black] (-0.5,0.05) -- (6.2,0.05);
  \node[c, red, anchor=west] at (-0.5,-0.4) {a2 fails in two models: not entailed};
\end{tikzpicture}
$$

By inspection, in every model where $KB$ is true, $\alpha_1$ is true; hence
$KB \models \alpha_1$ — there is no pit in $[1,2]$, and the agent may step there
safely. But in _some_ model where $KB$ is true, $\alpha_2$ is false; hence
$KB \not\models \alpha_2$ — the agent cannot yet conclude anything about $[2,2]$.
This procedure, enumerating every model and checking that $\alpha$ holds in all
those where $KB$ holds, is called **model checking**: it verifies
$M(KB) \subseteq M(\alpha)$ directly.

### Inference, soundness, completeness

Model checking is one _inference procedure_; there are others. If a procedure $i$
can derive $\alpha$ from $KB$ we write $KB \vdash_i \alpha$, read "$\alpha$ is
derived from $KB$ by $i$." Two properties separate the good procedures from the
dangerous.[^aima-sound] Picture the consequences of $KB$ as a haystack and
$\alpha$ as a needle: entailment is the needle being _in_ the haystack; inference
is the act of _finding_ it.

> **Definition (Soundness).** An inference procedure is **sound** (or
> truth-preserving) if it derives only entailed sentences: $KB \vdash_i \alpha$
> implies $KB \models \alpha$. An unsound procedure announces needles that are not
> in the haystack.

> **Definition (Completeness).** An inference procedure is **complete** if it can
> derive every entailed sentence: $KB \models \alpha$ implies
> $KB \vdash_i \alpha$. A complete procedure finds every needle that is really
> there.

Model checking is sound (it implements the definition of entailment) and, when
the space of models is finite, complete (it examines every one). These two
properties, together, are what make an inference procedure trustworthy: soundness
says its conclusions are true whenever the premises are, and completeness says it
never misses a conclusion the premises support. A sound procedure operating on
mere _syntax_ — bits in registers, symbols on a page — nonetheless yields
conclusions that hold in the real world, provided $KB$ itself is true of the
world. That correspondence between symbol-shuffling and reality is the reason
logic is worth building.

## Propositional logic

Propositional logic is the simplest logic rich enough to show all of this at
work. Its **syntax** is built from **proposition symbols** — $P$, $Q$, $R$,
$W_{1,3}$ — each standing for a proposition that is true or false. Two symbols
have fixed meaning: $\mathit{True}$, always true, and $\mathit{False}$, always
false. An **atomic sentence** is a single symbol; **complex sentences** are built
from simpler ones with five **connectives**, in order of precedence:[^aima-syntax]

| Connective | Name | Reads as |
| --- | --- | --- |
| $\lnot$ | negation | not |
| $\land$ | conjunction | and |
| $\lor$ | disjunction | or |
| $\Rightarrow$ | implication | implies / if–then |
| $\Leftrightarrow$ | biconditional | if and only if |

A **literal** is an atomic sentence (a positive literal) or its negation (a
negative literal). An implication $\alpha \Rightarrow \beta$ has a **premise** (or
antecedent) $\alpha$ and a **conclusion** (or consequent) $\beta$. The precedence
$\lnot, \land, \lor, \Rightarrow, \Leftrightarrow$ from highest to lowest lets
$\lnot A \land B$ mean $(\lnot A) \land B$; parentheses override it when needed.

The **semantics** fixes the truth of any sentence in a model. A model here simply
assigns $\mathit{true}$ or $\mathit{false}$ to every proposition symbol; with $n$
symbols there are $2^n$ models. `True` is true everywhere and `False` false
everywhere; every other symbol takes the value the model gives it. For complex
sentences, five rules compose truth from parts, in any model $m$:

- $\lnot P$ is true iff $P$ is false in $m$.
- $P \land Q$ is true iff both $P$ and $Q$ are true in $m$.
- $P \lor Q$ is true iff either $P$ or $Q$ (or both) is true in $m$.
- $P \Rightarrow Q$ is true unless $P$ is true and $Q$ is false in $m$.
- $P \Leftrightarrow Q$ is true iff $P$ and $Q$ have the same truth value in $m$.

The same rules read as a **truth table**, one row per assignment to the parts:

| $P$ | $Q$ | $\lnot P$ | $P \land Q$ | $P \lor Q$ | $P \Rightarrow Q$ | $P \Leftrightarrow Q$ |
| --- | --- | --- | --- | --- | --- | --- |
| F | F | T | F | F | T | T |
| F | T | T | F | T | T | F |
| T | F | F | F | T | F | F |
| T | T | F | T | T | T | T |

The one row that surprises people is $P \Rightarrow Q$ when $P$ is false:
implication is _true_ whenever its antecedent is false, so "5 is even implies Sam
is smart" is a true sentence of propositional logic. Read $P \Rightarrow Q$ as a
promise — "if $P$, then I claim $Q$" — that is broken only when $P$ holds and $Q$
fails. That is the only false row.

### A knowledge base for the Wumpus World

With semantics in hand we can encode the cave. For each square $[x,y]$ let
$P_{x,y}$ mean there is a pit, $W_{x,y}$ a wumpus, $B_{x,y}$ a perceived breeze,
$S_{x,y}$ a perceived stench. The immutable rules and the first two percepts
become a handful of labelled sentences:[^aima-kb]

$$
\begin{aligned}
R_1 &: \lnot P_{1,1} \\
R_2 &: B_{1,1} \Leftrightarrow (P_{1,2} \lor P_{2,1}) \\
R_3 &: B_{2,1} \Leftrightarrow (P_{1,1} \lor P_{2,2} \lor P_{3,1}) \\
R_4 &: \lnot B_{1,1} \\
R_5 &: B_{2,1}
\end{aligned}
$$

$R_1$ says the start is pitless; $R_2$ and $R_3$ say a square is breezy _if and
only if_ a neighbor has a pit — the biconditional matters, since a breeze both
implies and is implied by an adjacent pit; $R_4$ and $R_5$ are the observed
breezes. Now the question "is there a pit in $[1,2]$?" is the entailment query
$KB \models \lnot P_{1,2}$, and we already know the answer is yes.

### Model checking as an algorithm

The direct way to decide $KB \models \alpha$ is to enumerate models. With seven
symbols in the example there are $2^7 = 128$ of them; $KB$ is true in exactly
three, and $\lnot P_{1,2}$ holds in all three, so the entailment goes through.
`TT-Entails?` implements this as a recursive, depth-first enumeration over
assignments to the symbols — the same shape as backtracking search.[^aima-tt]

```algorithm
caption: $\textsc{TT-Entails?}$ — decide $KB \models \alpha$ by truth-table enumeration
input: $KB$, a sentence; $\alpha$, the query
$symbols \gets$ a list of the proposition symbols in $KB$ and $\alpha$
return $\textsc{TT-Check-All}(KB, \alpha, symbols, \{\,\})$

function $\textsc{TT-Check-All}(KB, \alpha, symbols, model)$
if $symbols$ is empty then
  if $\textsc{PL-True?}(KB, model)$ then
    return $\textsc{PL-True?}(\alpha, model)$
  else
    return $true$ // when KB is false, vacuously OK
else
  $P \gets \textsc{First}(symbols)$
  $rest \gets \textsc{Rest}(symbols)$
  return $\textsc{TT-Check-All}(KB, \alpha, rest, model \cup \{P = true\})$ and
    $\textsc{TT-Check-All}(KB, \alpha, rest, model \cup \{P = false\})$
```

`TT-Entails?` is sound because it implements the definition of entailment
directly, and complete because it always terminates — there are only finitely
many models. Its cost is the catch: $n$ symbols give $2^n$ models, so the time is
$O(2^n)$, though the depth-first recursion keeps space to $O(n)$. Propositional
entailment is co-NP-complete, so _every_ known inference algorithm has worst-case
exponential time. The rest of the lesson is a search for methods that win in the
common case even though they cannot win in the worst.

## Theorem proving

Model checking asks about every model. **Theorem proving** ignores models and
applies rules of inference directly to the sentences, building a _proof_ — a chain
of conclusions to the goal. When models are many but the proof is short, this is
far cheaper. Three concepts related to entailment set it up.[^aima-tp]

> **Definition (Logical equivalence).** Sentences $\alpha$ and $\beta$ are
> **logically equivalent**, $\alpha \equiv \beta$, if they are true in exactly the
> same models. Equivalently, $\alpha \equiv \beta$ iff $\alpha \models \beta$ and
> $\beta \models \alpha$.

> **Definition (Validity).** A sentence is **valid** (a **tautology**) if it is
> true in _all_ models, like $P \lor \lnot P$. Valid sentences are equivalent to
> $\mathit{True}$.

> **Definition (Satisfiability).** A sentence is **satisfiable** if it is true in
> _some_ model. Deciding satisfiability is the **SAT** problem — the first problem
> proved NP-complete.

The three concepts are tightly linked. Validity
ties to entailment through the **deduction theorem**, known to the ancient Greeks:

$$
\alpha \models \beta \quad\text{if and only if}\quad (\alpha \Rightarrow \beta)
\text{ is valid.}
$$

Satisfiability ties to entailment through its mirror image. A sentence is valid
iff its negation is unsatisfiable, which gives the result that powers every modern
prover:

$$
\alpha \models \beta \quad\text{if and only if}\quad (\alpha \land \lnot \beta)
\text{ is unsatisfiable.}
$$

Proving $\beta$ from $\alpha$ by showing $\alpha \land \lnot \beta$ has no model
is proof by **refutation** (or _reductio ad absurdum_): assume the negation of
what you want, and derive a contradiction. Deciding entailment thus reduces to
deciding _unsatisfiability_ — a single, uniform target.

### Inference rules and equivalences

A proof strings together **inference rules**. The best known is **Modus Ponens**:
from $\alpha \Rightarrow \beta$ and $\alpha$, infer $\beta$.

$$
\frac{\alpha \Rightarrow \beta, \quad \alpha}{\beta}
$$

**And-Elimination** infers either conjunct from a conjunction: from
$\alpha \land \beta$, infer $\alpha$. Every logical equivalence doubles as a pair
of inference rules — the standard set includes commutativity and associativity of
$\land$ and $\lor$, double-negation elimination $\lnot(\lnot\alpha) \equiv \alpha$,
contraposition, implication elimination
$(\alpha \Rightarrow \beta) \equiv (\lnot\alpha \lor \beta)$, biconditional
elimination, De Morgan's laws $\lnot(\alpha \land \beta) \equiv (\lnot\alpha \lor
\lnot\beta)$, and distributivity of $\land$ over $\lor$ and vice versa. Chaining
these rules by hand, the agent can prove $\lnot P_{1,2}$ from $R_1$ through $R_5$:
biconditional elimination on $R_2$, And-Elimination, contraposition, Modus Ponens
with the percept $R_4$, and finally De Morgan's law deliver
$\lnot P_{1,2} \land \lnot P_{2,1}$ — neither $[1,2]$ nor $[2,1]$ holds a pit.

A proof search over these rules can ignore irrelevant propositions no matter how
many there are — the proof above never mentions the far-off squares — which is
precisely why theorem proving can beat model checking. Adding a million unrelated
sentences leaves the proof untouched but multiplies the models exponentially. One
subtlety underwrites this: logic is **monotonic**. Adding sentences to $KB$ can
only _increase_ the set of entailed conclusions, never retract one:

$$
\text{if } KB \models \alpha \text{ then } KB \land \beta \models \alpha.
$$

An inference rule fires the moment its premises are present; its conclusion holds
regardless of whatever else the knowledge base contains.

## CNF and resolution

Modus Ponens and equivalences are sound, but a knowledge base can name rules that
are collectively too weak — no proof of an entailed sentence exists using only the
rules on hand — so the procedure is _incomplete_. One inference rule fixes this.
**Resolution**, coupled with any complete search, is a complete inference
procedure for all of propositional logic.[^aima-res]

Resolution operates on **clauses** — disjunctions of literals. The full rule takes
two clauses containing **complementary literals** (one the negation of the other)
and produces a new clause with all the literals of both, minus the complementary
pair:

$$
\frac{\ell_1 \lor \cdots \lor \ell_k, \qquad m_1 \lor \cdots \lor m_n}
{\ell_1 \lor \cdots \lor \ell_{i-1} \lor \ell_{i+1} \lor \cdots \lor \ell_k \lor
m_1 \lor \cdots \lor m_{j-1} \lor m_{j+1} \lor \cdots \lor m_n}
$$

where $\ell_i$ and $m_j$ are complementary. For instance $P_{1,1} \lor P_{3,1}$
resolved with $\lnot P_{1,1} \lor \lnot P_{2,2}$ yields
$P_{3,1} \lor \lnot P_{2,2}$. The resulting clause keeps only one copy of each
literal, a cleanup called **factoring**. Soundness is quick to see: the pivot
literal $\ell_i$ is either true or false; whichever it is, the surviving literals
of one clause or the other must carry the disjunction's truth.

Resolution applies only to clauses, so it would seem to cover only part of the
language. It covers all of it, because **every** propositional sentence is
equivalent to a conjunction of clauses — its **conjunctive normal form** (CNF).
The conversion is mechanical: eliminate $\Leftrightarrow$ and $\Rightarrow$ via
their equivalences, drive $\lnot$ inward with De Morgan's laws until it touches
only literals, then distribute $\lor$ over $\land$. Converting
$B_{1,1} \Leftrightarrow (P_{1,2} \lor P_{2,1})$ runs:

$$
\begin{aligned}
&(B_{1,1} \Rightarrow (P_{1,2} \lor P_{2,1})) \land ((P_{1,2} \lor P_{2,1})
  \Rightarrow B_{1,1}) \\
&(\lnot B_{1,1} \lor P_{1,2} \lor P_{2,1}) \land (\lnot(P_{1,2} \lor P_{2,1})
  \lor B_{1,1}) \\
&(\lnot B_{1,1} \lor P_{1,2} \lor P_{2,1}) \land (\lnot P_{1,2} \lor B_{1,1})
  \land (\lnot P_{2,1} \lor B_{1,1}).
\end{aligned}
$$

The three stages — eliminate the biconditional, drive negations inward,
distribute — reappear unchanged as the pipeline for
[first-order sentences](/artificial-intelligence/logic-and-planning/inference-and-resolution),
minus the skolemization step that only quantifiers need. It always terminates and
always produces an equivalent conjunction of clauses.

$$
% caption: The CNF conversion pipeline, run on $B_{1,1} \Leftrightarrow (P_{1,2}
% \lor P_{2,1})$. Each stage rewrites the sentence with a fixed equivalence; the
% output is a conjunction of three clauses. In propositional logic there is no
% skolemization step, which is the one stage that separates this from the
% first-order conversion.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  st/.style={draw, minimum width=34mm, minimum height=8mm, align=center, font=\scriptsize}]
  \definecolor{acc}{HTML}{2348F2}
  \node[st] (s1) at (0,0)     {biconditional to two $\Rightarrow$};
  \node[st] (s2) at (0,-1.15) {$\Rightarrow$ to (not .. or ..)};
  \node[st] (s3) at (0,-2.3)  {De Morgan: not inwards};
  \node[st, draw=acc, text=acc, thick] (s4) at (0,-3.45) {distribute or over and};
  \node[st] (s5) at (0,-4.6)  {list the clauses};
  \foreach \a/\b in {s1/s2, s2/s3, s3/s4, s4/s5}
    \draw[->, acc, thick] (\a) -- (\b);
  \node[anchor=west, text=black, font=\scriptsize, align=left] at (2.3,-3.45)
    {the only step that\\can grow the sentence};
\end{tikzpicture}
$$

### The resolution algorithm

To decide $KB \models \alpha$, refute: show $KB \land \lnot\alpha$ is
unsatisfiable. `PL-Resolution` converts $KB \land \lnot\alpha$ to CNF, then
resolves every pair of clauses with complementary literals, adding each new clause
back into the pool. Two things can end it. If a pair resolves to the **empty
clause** — a disjunction of no literals, equivalent to $\mathit{False}$ — then
$KB \land \lnot\alpha$ is contradictory and $KB \models \alpha$. If no new clause
can be added, the empty clause never appears and $KB \not\models \alpha$.

```algorithm
caption: $\textsc{PL-Resolution}$ — decide $KB \models \alpha$ by refutation
input: $KB$, a sentence; $\alpha$, the query
$clauses \gets$ the set of clauses in the CNF of $KB \land \lnot\alpha$
$new \gets \{\,\}$
loop
  for each pair of clauses $C_i, C_j$ in $clauses$ do
    $resolvents \gets \textsc{PL-Resolve}(C_i, C_j)$
    if $resolvents$ contains the empty clause then
      return $true$ // contradiction found: KB entails $\alpha$
    $new \gets new \cup resolvents$
  if $new \subseteq clauses$ then
    return $false$ // no progress: KB does not entail $\alpha$
  $clauses \gets clauses \cup new$
```

The algorithm terminates because only finitely many distinct clauses can be built
from finitely many symbols — the factoring step is what keeps that count finite.
Its completeness is the **ground resolution theorem**: if a set of clauses is
unsatisfiable, the closure of the clauses under resolution contains the empty
clause. So a resolution prover can decide $\alpha \models \beta$ for any
propositional $\alpha, \beta$ — a general, complete method, at the cost of
CNF conversion and a possibly large clause pool.

### A resolution refutation, worked

Take the wumpus fragment and prove $KB \models \lnot P_{1,2}$ by refutation. The
relevant clauses of $KB$ come from $R_2$, $R_4$ ($\lnot B_{1,1}$), and the added
negated goal $P_{1,2}$. Converting $R_2 = B_{1,1} \Leftrightarrow (P_{1,2} \lor
P_{2,1})$ to CNF gives the three clauses derived above; the one we need is
$C_a = \lnot P_{1,2} \lor B_{1,1}$. Add $C_b = \lnot B_{1,1}$ (the percept $R_4$)
and $C_g = P_{1,2}$ (the negated query). Resolution now runs a two-step spine:

$$
\begin{aligned}
C_a = \lnot P_{1,2} \lor B_{1,1},\quad C_g = P_{1,2} \;&\xrightarrow{\text{resolve on } P_{1,2}}\; B_{1,1}, \\
B_{1,1},\quad C_b = \lnot B_{1,1} \;&\xrightarrow{\text{resolve on } B_{1,1}}\; \square.
\end{aligned}
$$

The empty clause $\square$ appears, so $KB \land P_{1,2}$ is unsatisfiable and
$KB \models \lnot P_{1,2}$ — the same conclusion model checking reached, now by
symbol-shuffling that never enumerated a single model.

$$
% caption: The resolution refutation of $KB \models \lnot P_{1,2}$. The negated
% goal $P_{1,2}$ resolves against a clause of $R_2$ to produce $B_{1,1}$, which
% resolves against the percept $\lnot B_{1,1}$ to yield the empty clause (box),
% the mark of contradiction.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  cl/.style={draw, minimum height=6mm, inner sep=3pt, font=\scriptsize, align=center},
  sp/.style={draw=acc, text=acc, thick, minimum height=6mm, inner sep=3pt, font=\scriptsize, align=center}]
  \definecolor{acc}{HTML}{2348F2}
  \node[cl] (ca) at (0,2.4)   {not P12 or B11};
  \node[sp] (cg) at (4.4,2.4) {P12 (negated goal)};
  \node[sp] (b)  at (2.2,1.1) {B11};
  \node[cl] (cb) at (5.0,1.1) {not B11};
  \node[draw=acc, text=acc, thick, minimum size=5mm, inner sep=1pt] (box) at (3.6,-0.2) {\ };
  \draw[->, acc, thick] (ca) -- (b);
  \draw[->, acc, thick] (cg) -- (b);
  \draw[->, acc, thick] (b) -- (box);
  \draw[->, acc, thick] (cb) -- (box);
  \node[font=\scriptsize, text=black, anchor=west] at (4.2,-0.2) {contradiction};
\end{tikzpicture}
$$


## Where this continues

We now have two complete ways to decide $KB \models \alpha$: enumerate models with
`TT-Entails?`, or refute $KB \land \lnot\alpha$ with resolution. Both are sound and
complete, and both can be exponential in the worst case. What is left is the
engineering that makes inference fast in the common case, and the machinery that
turns a static knowledge base into a _situated_ agent acting over time.

This continues in
[Propositional Inference and Logical Agents](/artificial-intelligence/logic-and-planning/propositional-inference),
which develops the linear-time Horn-clause chaining behind logic programming, the
DPLL and WalkSAT solvers that make model checking practical, and the time-indexed
fluents, successor-state axioms, and SATPlan reduction that let a propositional
agent perceive, remember, and plan.

[^aima-intro]: **AIMA**, Ch. 7 — Logical Agents; §7.1 Knowledge-Based Agents: intelligence as reasoning over internal representations, the $KB$ of sentences, and the `Tell`/`Ask` interface with its requirement that answers follow from what was told.
[^aima-wumpus]: **AIMA**, §7.2 The Wumpus World: the PEAS description, the five percepts (stench, breeze, glitter, bump, scream), and the worked sequence of deductions the agent makes from its first moves.
[^aima-logic]: **AIMA**, §7.3 Logic: syntax versus semantics, models as mathematical fixings of truth, $M(\alpha)$ for the set of models of $\alpha$, and satisfaction.
[^aima-entail]: **AIMA**, §7.3 Logic: entailment defined as $M(\alpha) \subseteq M(\beta)$, the pit example with $\alpha_1, \alpha_2$, and model checking as $M(KB) \subseteq M(\alpha)$.
[^aima-sound]: **AIMA**, §7.3 Logic: the derivation notation $KB \vdash_i \alpha$, the haystack-and-needle picture, and soundness (truth-preserving) versus completeness.
[^aima-syntax]: **AIMA**, §7.4.1 Syntax; §7.4.2 Semantics: proposition symbols, the five connectives with their precedence, literals, models as truth assignments, and the truth tables.
[^aima-kb]: **AIMA**, §7.4.3 A Simple Knowledge Base: the symbols $P_{x,y}, W_{x,y}, B_{x,y}, S_{x,y}$ and the sentences $R_1$ through $R_5$ encoding the immutable rules and the first percepts.
[^aima-tt]: **AIMA**, §7.4.4 A Simple Inference Procedure: `TT-Entails?` and `TT-Check-All`, soundness and completeness by finite enumeration, the $O(2^n)$ cost, and co-NP-completeness of propositional entailment.
[^aima-tp]: **AIMA**, §7.5 Propositional Theorem Proving: logical equivalence, validity and tautologies, satisfiability and SAT, the deduction theorem, and the refutation identity $\alpha \models \beta$ iff $\alpha \land \lnot\beta$ is unsatisfiable; §7.5.1 inference rules; monotonicity.
[^aima-res]: **AIMA**, §7.5.2 Proof by Resolution: the resolution rule, complementary literals, factoring, conversion to CNF, `PL-Resolution` by refutation, the resolution closure, and the ground resolution theorem.