Logical Agents and Propositional Logic

The search 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.¹ 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 Asks a question, the answer must follow from what has been Telled.

Each time the agent program runs, it does three things: it Tells the $KB$ what it just perceived; it Asks 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 Tells the $KB$ which action it chose, before executing it. Written out, the loop is short — the intelligence is hidden inside Ask.

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 Telling 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.²

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.

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.³ 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

In words: $\alpha \models \beta$ exactly when, in every model where $\alpha$ is true, $\beta$ is true as well.⁴ 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.

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]$:q and ${\alpha }_2=$no pit in $[2,2]$".

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 $\neg 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}=false$ and $(p_{22}\vee p_{31})$ true.

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/\models {\alpha }_2$.

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/\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{⊢}_i\alpha$, read $\alpha$ is derived from $KB$ by $i$. Two properties separate the good procedures from the dangerous.⁵ 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.

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: $True$, always true, and $False$, always false. An atomic sentence is a single symbol; complex sentences are built from simpler ones with five connectives, in order of precedence:⁶

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 $\neg ,\wedge ,\vee ,\Rightarrow ,\iff$ from highest to lowest lets $\neg A\wedge B$ mean $(\neg A)\wedge B$; parentheses override it when needed.

The semantics fixes the truth of any sentence in a model. A model here simply assigns $true$ or $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$:

• $\neg P$ is true iff $P$ is false in $m$.
• $P\wedge Q$ is true iff both $P$ and $Q$ are true in $m$.
• $P\vee 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\iff 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:

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:⁷

$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 \neg 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 $\neg 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.⁸

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.⁹

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

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:

Proving $\beta$ from $\alpha$ by showing $\alpha \wedge \neg \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$.

And-Elimination infers either conjunct from a conjunction: from $\alpha \wedge \beta$, infer $\alpha$. Every logical equivalence doubles as a pair of inference rules — the standard set includes commutativity and associativity of $\wedge$ and $\vee$, double-negation elimination $\neg (\neg \alpha )\equiv \alpha$, contraposition, implication elimination $(\alpha \Rightarrow \beta )\equiv (\neg \alpha \vee \beta )$, biconditional elimination, De Morgan's laws $\neg (\alpha \wedge \beta )\equiv (\neg \alpha \vee \neg \beta )$, and distributivity of $\wedge$ over $\vee$ and vice versa. Chaining these rules by hand, the agent can prove $\neg 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 $\neg P_{1,2}\wedge \neg 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:

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.¹⁰

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:

where ${\ell }_i$ and $m_j$ are complementary. For instance $P_{1,1}\vee P_{3,1}$ resolved with $\neg P_{1,1}\vee \neg P_{2,2}$ yields $P_{3,1}\vee \neg 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 $\iff$ and $\Rightarrow$ via their equivalences, drive $\neg$ inward with De Morgan's laws until it touches only literals, then distribute $\vee$ over $\wedge$. Converting $B_{1,1}\iff (P_{1,2}\vee P_{2,1})$ runs:

The three stages — eliminate the biconditional, drive negations inward, distribute — reappear unchanged as the pipeline for first-order sentences, minus the skolemization step that only quantifiers need. It always terminates and always produces an equivalent conjunction of clauses.

The resolution algorithm

To decide $KB\models \alpha$, refute: show $KB\wedge \neg \alpha$ is unsatisfiable. PL-Resolution converts $KB\wedge \neg \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 $False$ — then $KB\wedge \neg \alpha$ is contradictory and $KB\models \alpha$. If no new clause can be added, the empty clause never appears and $KB/\models \alpha$.

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 \neg P_{1,2}$ by refutation. The relevant clauses of $KB$ come from $R_2$, $R_4$ ($\neg B_{1,1}$), and the added negated goal $P_{1,2}$. Converting $R_2=B_{1,1}\iff (P_{1,2}\vee P_{2,1})$ to CNF gives the three clauses derived above; the one we need is $C_a=\neg P_{1,2}\vee B_{1,1}$. Add $C_b=\neg B_{1,1}$ (the percept $R_4$) and $C_g=P_{1,2}$ (the negated query). Resolution now runs a two-step spine:

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

Where this continues

We now have two complete ways to decide $KB\models \alpha$: enumerate models with TT-Entails?, or refute $KB\wedge \neg \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, 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.