—

Artificial Computational Intelligence

Inference Techniques in Propositional Logic

Published: 2026-08-13

Level: postgraduate

Audience: Postgraduate students in Artificial Intelligence

Prerequisite Knowledge

This lecture builds on several concepts from earlier sessions. If any feel unfamiliar, review the earlier notes before proceeding.

Previously Covered in This Subject

Knowledge-based agents — covered in Lecture 9 (Knowledge Representation Using Logics)
The Wumpus world — covered in Lecture 9 (Knowledge Representation Using Logics)
Entailment and models — covered in Lecture 9 (Knowledge Representation Using Logics)
Propositional logic connectives and truth tables — covered in Lecture 9 (Knowledge Representation Using Logics)
Inference by truth table — covered in Lecture 9 (Knowledge Representation Using Logics)
Logical equivalences and inference rules — covered in Lecture 9 (Knowledge Representation Using Logics)

10.1 Knowledge-Based Agents and the Inference Problem

10.1.1 The Knowledge Base and the Query

The question that starts everything: how can a machine gain new knowledge that nobody typed into it? The answer for this module: not by magic, but by inference — taking statements it already has and combining them to get statements it did not have. "How can we infer new knowledge? So that's the whole art of this topic, that we are given a bunch of things, and how do we infer from those given data some new rules? And this is very fundamental to AI."

We are continuing the knowledge representation module. The central picture from the previous session: an agent lives in a world it does not fully observe, it holds a set of statements it knows for sure, and its whole job is to answer questions about what it has not directly observed. That store of known statements is the knowledge base (KB, the set of sentences the agent accepts as true). A query is any statement we ask the agent to decide — true, false, or unknown. The loop that makes a knowledge-based agent actually learn: the agent starts with a KB, it is asked a query, it runs some inference technique to decide whether the query follows from the KB, and once it knows the answer, that answer is itself new insight that gets added back into the KB. In this way the agent incrementally builds its knowledge: "it has a set of knowledge base to begin with, and then it will keep using some of this inferencing and queries. And when it knows the answer for a query, that also becomes an insight, that also becomes knowledge, and we can put that into the knowledge base."

The technical name for the relationship we are checking is entailment — one statement following from another. We write

$KB ⊨ α$

and read it as "the knowledge base entails alpha". Here $KB$ is the knowledge base (a sentence standing for all the agent's rules, joined by AND), $α$ (alpha) is the query, and $⊨$ is the entailment symbol. The meaning: every assignment of truth values that makes every rule in the KB true also makes the query $α$ true. In set language, if $M (KB)$ is the set of models (truth-value assignments) in which the KB is true and $M (α)$ the set in which the query is true, then entailment says

$KB ⊨ α iff M (KB) \subseteq M (α)$

Every assignment the KB allows, the query also allows. The session's own example will be the statement "negation P1,2" — $\neg P_{1, 2}$ — as the query: does the knowledge base entail that there is no pit at cell (1,2)?

Entailment (the definition): $KB ⊨ α$ means "every model of the KB is also a model of $α$ ". Equivalently: there is no assignment of true/false to the literals under which all the KB's rules are true but the query is false. If such an assignment existed, the KB would not entail the query — the query would be unknown.

Everyday analogy — the detective's case file. Picture a detective with a file folder of confirmed facts and rules: "the butler was in the kitchen", "anyone in the kitchen at 8 p.m. heard the door". The folder is the KB. A claim like "the butler heard the door" is entailed when every complete scenario consistent with the folder forces the claim to be true. If at least one consistent scenario leaves the claim open, the file does not prove it. Where the analogy breaks: a detective can accept "very likely" — logic has no such middle ground, only true, false, or not decided.

Why does this matter for AI at all? Because modern AI systems infer in different technical ways, but "it all boils down to this" — inferencing techniques where, given a set of rules, we deduce new information.

10.1.2 The Wumpus World Problem Setup

The running example is the Wumpus world — a classic AI test environment: a grid-world cave that contains a wumpus (a beast), pits, and gold. We never discuss the creature itself today; what matters is the sensing model. A breeze at a cell signals that a pit is in a neighboring cell (directly adjacent, not diagonal). The agent knows five facts, numbered R1 to R5, with positions written as (row, column), so $P_{1, 2}$ means "there is a pit at cell (1,2)":

$R_{1} = \neg P_{1, 1}$ — no pit at (1,1).
$R_{2} = B_{1, 1} ⟺ (P_{1, 2} \lor P_{2, 1})$ — there is a breeze at (1,1) exactly when there is a pit at (1,2) or at (2,1).
$R_{3} = B_{2, 1} ⟺ (P_{1, 1} \lor P_{2, 2} \lor P_{3, 1})$ — a breeze at (2,1) exactly when one of the three pits $P_{1, 1}, P_{2, 2}, P_{3, 1}$ exists.
$R_{4} = \neg B_{1, 1}$ — no breeze at (1,1).
$R_{5} = B_{2, 1}$ — there is a breeze at (2,1).

The query we keep returning to all session is $\neg P_{1, 2}$ : "there is no pit at (1,2)" — is it true given these five rules? Read aloud, $R_{2}$ says "B11 double implies P12 or P21": a breeze at (1,1) forces a pit at (1,2) or (2,1), and a pit at either of those cells forces a breeze at (1,1). The symbols $P$ (pit) and $B$ (breeze) with two subscripts are called literals — single propositional facts that can be true or false. A literal is an atomic sentence (like $P_{1, 2}$ ) or its negation (like $\neg P_{1, 2}$ ). The full set of literals in this problem is $P_{1, 1}, P_{1, 2}, P_{2, 1}, P_{2, 2}, P_{3, 1}, B_{1, 1}, B_{2, 1}$ — seven of them, a number that will matter in the next section.

Visualize the cave. Picture a 4×4 grid of rooms with the agent starting in the bottom-left corner, cell (1,1). The cells touching (1,1) are (1,2) on its right and (2,1) above it. The cells touching (2,1) are (1,1), (2,2), and (3,1). So $R_{2}$ says: breeze at (1,1) means a pit in the two rooms it touches; $R_{3}$ says: breeze at (2,1) means a pit in the three rooms it touches. The sensors report: no breeze at (1,1), breeze at (2,1). From these five rules alone the agent must decide whether (1,2) hides a pit.

Why not write these rules in plain English and reason in English? Because the agent must evaluate and deduce mechanically; English sentences are too loose for that. "We can't be putting them in plain English sentences. We need to be evaluating, deducing, and so on. So, it's better we use a standard notation, and that is where we told we will use logic." And logic is not an AI invention — it is a general concept from discrete mathematics, split into propositional logic (this session) and predicate logic (coming up). The previous class already covered the details of propositional logic, including its truth tables (the professor calls them "group tables").

Scope of the setting: this entire session assumes propositional logic — every literal is a single true-or-false fact, and the KB is a collection of such facts joined by connectives. The rules R1–R5 must all be consistent with each other; if the KB ever contained a literal and its negation at the same time (say $P_{1, 2}$ and $\neg P_{1, 2}$ ), the KB would be inconsistent, and then every query would look "entailed" because no assignment could satisfy the KB at all — a degenerate case that produces no useful information. The notation itself assumes positions are read as (row, column), and that the OR inside $R_{2}$ and $R_{3}$ is the inclusive OR of logic (at least one pit), not the exclusive OR of everyday English ("exactly one").

The assumptions above are what the rules mean. Mistakes in writing the rules down are a different matter, and four of them show up again and again when students first try this setup:

Common traps in the setup:

Swapping the subscripts. $P_{1, 2}$ and $P_{2, 1}$ are different cells. Read each literal as (row, column), always in that order — the whole derivation later depends on it.
Reading "iff" as one direction only. $B_{1, 1} ⟺ (P_{1, 2} \lor P_{2, 1})$ is two implications packed into one: breeze forces a pit and a pit forces breeze. Later we split it precisely because both directions matter.
Reading OR as "exactly one". In logic, $P_{1, 2} \lor P_{2, 1}$ is true even if both cells have pits.
Forgetting the number of literals. Seven literals is small enough to list; count them before starting any technique, because the count drives the cost of the first technique.

10.1.3 Why We Need More Than One Technique

The session is framed around one honest observation: the truth table approach works, but it is brutally expensive. Seven literals give $2^{7} = 128$ rows, and real problems have many more literals. So the session builds a ladder of techniques, each improving on the last:

Truth table inferencing (recap) — exhaustive, simple, exponential.
Theorem proving with logical equivalences — fast when you choose rules well.
Proof by contradiction — the trick of proving the negation instead.
PL resolution with CNF — a mechanical rule-based version of contradiction.
DPLL — a backtracking search that finds the satisfying rows without building the table.

And the why of it all: "Why are we doing all this on a Sunday morning? We want our agent to learn. It wants to infer new things and add it into its knowledge base." The agent asks "is there a pit at (1,2) or not", the technique answers, and "once it knows if there is pit or not, that is a knowledge for the agent."

When does a knowledge-based agent actually get used? Rule-based diagnosis is the textbook case: network fault diagnosis systems hold rules like "if a server is unreachable and its router is down, the fault is at the router", and a query like "is the router down?" is answered by checking entailment against the symptom rules. The same pattern appears in configuration verifiers, compliance checkers, and the symbolic reasoning components of modern planning systems. In each case the agent's learning is exactly the loop above: answer a query, add the answer to the KB, answer the next query with more knowledge than before.

Recap: a knowledge-based agent answers queries by checking what its KB entails; the Wumpus world gives us a concrete five-rule KB and one stubborn query, $\neg P_{1, 2}$ . Five techniques, from the brute-force truth table to the clever DPLL search, will all try to answer that same query — and they will all agree. The ladder starts with the truth table in the next section.

10.2 Truth Table Inferencing

10.2.1 The 128-Row Truth Table

The first technique, recapped from the previous session, is truth table inferencing — the brute-force baseline every other technique is compared against. The procedure has a fixed shape:

The truth table procedure:

Collect every literal in the knowledge base. Here there are exactly seven: $P_{1, 1}, P_{1, 2}, P_{2, 1}, P_{2, 2}, P_{3, 1}, B_{1, 1}, B_{2, 1}$ .
With $n$ literals the table has $2^{n}$ rows — every combination of true/false for every literal. For seven literals that is $2^{7} = 128$ rows.
Evaluate the validity of every rule $R_{1}$ through $R_{5}$ in each row. "We should also find the validity of all the rules that are given in my knowledge base. And then we should AND them, and that will give me the validity of the complete knowledge base."
Keep only the rows where the whole KB is true. In the last session we found exactly three such rows out of the 128.
Look at the query $\neg P_{1, 2}$ in those three rows only. In all three, $P_{1, 2}$ came out false, which makes $\neg P_{1, 2}$ true, true, true. The query holds in every model of the KB, so we claim $\neg P_{1, 2}$ is entailed — there is no pit at (1,2).

Worked example: the truth-table run for the Wumpus KB.

The literals are the seven facts $P_{1, 1}, P_{1, 2}, P_{2, 1}, P_{2, 2}, P_{3, 1}, B_{1, 1}, B_{2, 1}$ , so the table has $2^{7} = 128$ rows — write the seven literals as column headers and generate every pattern of T and F: row 1 all false, row 2 with $P_{1, 1}$ true only, and so on through all 128 combinations.

For each row, evaluate the five rules:

$R_{1} = \neg P_{1, 1}$ is true exactly when $P_{1, 1}$ is false.
$R_{2} = B_{1, 1} ⟺ (P_{1, 2} \lor P_{2, 1})$ is true when the breeze column and the (P12 OR P21) column agree.
$R_{3} = B_{2, 1} ⟺ (P_{1, 1} \lor P_{2, 2} \lor P_{3, 1})$ is true when the B2,1 column and the three-literal OR column agree.
$R_{4} = \neg B_{1, 1}$ requires $B_{1, 1}$ false; $R_{5} = B_{2, 1}$ requires $B_{2, 1}$ true.

AND the five rule columns: the KB column is true only where $R_{1}$ through $R_{5}$ are all true. Exactly 3 of the 128 rows pass. In those three rows, the $P_{1, 2}$ column reads false, false, false — so the query $\neg P_{1, 2}$ reads true, true, true.

Conclusion: the query is true in every model of the KB, so $KB ⊨ \neg P_{1, 2}$ — there is no pit at (1,2).

Sense-check: the answer matches the rules themselves. $R_{4}$ says there is no breeze at (1,1), and $R_{2}$ ties a breeze at (1,1) to a pit at (1,2) or (2,1) — so the rows that survive the rules should indeed keep $P_{1, 2}$ and $P_{2, 1}$ in check.

The summary of the whole approach: "take all the literals given in my knowledge base and draw the truth table, and then in that truth table, go and check your query where all the rules are true."

10.2.2 Exponential Cost and When It Fails

The technique is simple and always correct, but the cost is the problem: "if the number of literals are increasing, then the truth table will just explode." Seven literals already gave 128 rows, and "for bigger real world use cases the truth table will be really huge and it is a exponential time complexity and we cannot always go for this approach." Each new literal doubles the table, so the growth is

$2^{n}$

— exponential no matter how you count it. With $n = 20$ literals the table already has $2^{20} = 1, 048, 576$ rows; with $n = 50$ it has roughly $1 0^{15}$ — more rows than can be written down. The technique stays sound (it never claims a false entailment) and complete (it answers every query), but the price of that certainty is the full enumeration.

There is also a conceptual waste hidden in the table. Of the 128 rows, only 3 were actually used; the other 125 rows existed only to be discarded. The fix is teased early: "Why should we draw all the 128 rows if it's anyway useless? We are only bothered about those 3 rows where everything is true. So can we get there directly without enumerating all the rows?" That direct route is the DPLL algorithm, an idea conceived roughly 70 years back (in the 1950s) that we will study at the end of this session.

Visual intuition. Picture the table as a tall grid: 128 horizontal rows, one per assignment, with the seven literal columns on the left and the five rule columns (R1–R5) plus a final KB column on the right. Down that last column, 125 rows read false and exactly 3 read true — three tiny islands of "KB true" in a sea of discarded assignments. The whole table exists only to find those three rows.

Scope: when the truth table is usable and when it is not. The method applies to any finite propositional knowledge base — the KB here is finite because the literal list is finite. It breaks on scale: the row count is $2^{n}$ , so every extra literal doubles the work, and real-world knowledge bases with dozens of literals are out of reach. It also assumes you can list all literals up front; if the problem has quantifiers ("all", "some") it is outside propositional logic altogether and the table cannot even be built. As a practical rule, keep the truth table for tiny toy problems and verification, and switch to the upcoming techniques for anything bigger.

10.2.3 Student Questions and Answers

Exam note: the exam is open book — the rule book will be available, so the emphasis falls on understanding and applying the techniques correctly, not on memorizing. For anyone unsure about an equivalence rule, there is a safe private check: write both sides of the rule for the four combinations of true and false, and compare the columns.

Q: Is it a rule that we only need to take the rows where the knowledge base is true and ignore the others? A: Yes — you check your query only in the rows where all the rules of the knowledge base are true, and you ignore all the other rows. But even to get there you have to first draw the whole truth table, because only then do you know which rows make the knowledge base true. That is exactly why the DPLL algorithm exists: it reaches those three rows directly, without drawing all 128.

Recap: the truth table is the guaranteed-but-expensive baseline: sound, complete, and exponential in the literal count. The query is true in every model of the knowledge base — that is exactly what it means for the knowledge base to entail the query. The question that remains is whether we can reach those satisfying assignments directly, without enumerating the other 125.

10.3 Logical Equivalences and Inference Rules

10.3.1 The Rule Book

The second technique builds on a collection of logical equivalences — pairs of statements that are always interchangeable because their truth tables match. These were given as self-study, and a week-day webinar on logic covered them too (the webinar material also helps with the assignment). The professor read the whole rule book out loud: commutative, associative, double negation, De Morgan's laws, and then the two that get used constantly, modus ponens and and-elimination. In the worked problem we will also pull in biconditional elimination, implication elimination, and contraposition.

The equivalences, in symbols. Here $α$ and $β$ (and $γ$ ) are any propositions — the rules hold for every choice of statement, which is what "equivalent" means:

Double negation: $\neg\neg α \equiv α$ — two negations cancel.
De Morgan's laws: $\neg (α \land β) \equiv (\neg α \lor \neg β)$ and $\neg (α \lor β) \equiv (\neg α \land \neg β)$ — negation distributes by flipping the connective.
Commutativity: $α \land β \equiv β \land α$ and $α \lor β \equiv β \lor α$ — order inside a conjunction or disjunction does not matter.
Associativity: $(α \land β) \land γ \equiv α \land (β \land γ)$ , and the same for $\lor$ — grouping does not matter.
Biconditional elimination: $α ⟺ β \equiv (α \Rightarrow β) \land (β \Rightarrow α)$ — "double implies" splits into two single implications.
Implication elimination: $α \Rightarrow β \equiv \neg α \lor β$ — an implication can be rewritten as a disjunction.
Contraposition: $α \Rightarrow β \equiv \neg β \Rightarrow \neg α$ — an implication is equivalent to its contrapositive.

The framing for the whole book: "it's from basic math, where LHS and RHS are same" — every LHS statement is logically equivalent to its corresponding RHS, and "one way to convince yourself that all of these are correct is you can take alpha, beta and put that true true, true false, false true, false false, and try to compute the LHS in one column, RHS in one column and try to compare them and they'll be same." There is also a pure mathematics textbook (not an AI book) mentioned from the previous session where every one of these equivalences is proved and shown; it doubles as a practice source with many worked theorem-proving problems.

Worked check: contraposition, row by row. Take the rule $α \Rightarrow β \equiv \neg β \Rightarrow \neg α$ and run all four combinations of the two letters. Write a column for the left side and a column for the right side:

$α$	$β$	$α \Rightarrow β$	$\neg β \Rightarrow \neg α$
T	T	T	F $\Rightarrow$ F = T
T	F	F	T $\Rightarrow$ F = F
F	T	T	F $\Rightarrow$ T = T
F	F	T	T $\Rightarrow$ T = T

The two columns read T, F, T, T — identical. The left side and the right side are true in exactly the same models, so the equivalence holds. The same four-row comparison works for every rule in the book; that is the private check the professor suggested for anyone unsure about any equivalence.

Analogy — rewrite rules in arithmetic. Equivalences play the same role in logic that algebraic identities play in math: " $a + b = b + a$ " lets you swap the order of any addition, and " $α \lor β \equiv β \lor α$ " lets you swap the order of any disjunction, no matter how large the statement. An equivalence is a two-way street: whenever you see one side anywhere, you may replace it with the other side. Where the analogy strains: arithmetic keeps its numbers, while logic rules keep whole statements — and logic rules, unlike arithmetic facts, never have hidden conditions about the values involved.

10.3.2 Modus Ponens and And-Elimination in Plain Words

Two rules deserve extra attention because they do not just rewrite a statement — they let you extract a new fact.

Modus ponens (Latin for "mode that affirms", the classical rule of inference): if $α \Rightarrow β$ is given and $α$ itself is given, you may infer $β$ . The example: statement one says "if I am tired, then I need to rest" — that is $α \Rightarrow β$ with $α$ = "I am tired" and $β$ = "I need to rest". Statement two says "I am tired" — that is $α$ , given directly. From the two together: "I need to rest" — that is $β$ . The rule: "if there are two statements given, which is one is of the form alpha implies beta, and the second one is alpha itself, then I can infer that beta."

And-elimination: if $α \land β$ is given as true, then $α$ alone is true and $β$ alone is true. Why? In the truth table of AND, the conjunction is true only when both operands are true; so if you are told " $α$ and $β$ is true", each of them separately must be true. Example: given "I am tired and sleepy", you may separately conclude "I am tired" and "I am sleepy". The phrasing: "if alpha and beta are true, I can tell that alpha alone is true, beta alone is true."

The two extraction rules, in symbols:

$\frac{α \Rightarrow β α}{β} (modus ponens)$

Given an implication and its premise, the conclusion follows.

$\frac{α \land β}{α} \frac{α \land β}{β} (and-elimination)$

Given a conjunction, either conjunct follows on its own.

Both rules are sound — the truth table of $\Rightarrow$ has exactly one false row (true premise, false conclusion), so when $α$ is true and the implication holds, $β$ cannot be false; and the truth table of $\land$ is true only in the row where both parts are true.

Scope: when these rules apply and when they do not. Every equivalence in the book applies to any propositions — $α$ and $β$ may themselves be large compound statements, not just single literals. The extraction rules also apply to any matching shapes. But the rules are one-directional in use: modus ponens takes two premises and yields one conclusion, and you cannot run it in reverse — from $β$ and $α \Rightarrow β$ you may not infer $α$ (the implication is also true when both sides are false). And an implication must match the whole shape $α \Rightarrow β$ ; a statement that merely contains an implication inside a larger expression needs the equivalences first, not modus ponens.

10.3.3 How the Rules Connect to the Exam

Two practical notes were dropped here. First, the exam is open book: "You will have all this access, so no need to worry about it." Second, the name of each rule matters — a point that comes up again in the worked example, because each step must state which rule justifies it ("names will be required, otherwise we'll not even know what we are inferring").

Common traps in the rule book:

Applying a rule in the wrong direction. Modus ponens needs the premise $α$ as a second statement; having only the implication and the conclusion does not license anything.
Confusing $\equiv$ with $⟺$ . The double turnstile-free symbol $\equiv$ is a claim about two sentences (their truth tables match); $⟺$ is a connective inside a sentence. " $α \equiv β$ " and " $α ⟺ β$ " are related but different objects.
Forgetting the name of the rule you used. Every step of a proof must be justified by name; graders and the professor expect "modus ponens", "De Morgan", "and-elimination" written at each line.
Assuming an implication is false when the premise is false. $α \Rightarrow β$ is false only in the T $\Rightarrow$ F case; in every other row it is true. The tired-example rule depends on this.

Exam note: the rule book is provided at the exam, so the memory burden is light — but only if you can apply each rule and name it correctly. The professor's own advice: verify any doubtful equivalence privately with a four-row truth table, and get fluent with the two extraction rules, because they drive the theorem-proving examples.

The rule book also has a life outside this course: the same equivalences are the standard tools for simplifying Boolean expressions in digital circuit design — De Morgan's laws and distributivity are exactly what hardware engineers use to shrink logic circuits, and the manual simplification technique known as a Karnaugh map relies on the same equivalence facts. The pure mathematics textbook from the previous session remains the best practice ground: "you can keep practicing" with its worked theorem-proving problems, since the very next technique is a real proof.

Recap: equivalences rewrite statements without changing their meaning; modus ponens and and-elimination extract brand-new facts from what is already known. Armed with this rule book — including the always-useful modus ponens — we can now do theorem proving, the technique we had started in the last class and paused.

10.4 Theorem Proving by Logical Inference

10.4.1 The Worked Derivation: From R2 to R11

The same Wumpus problem that took a 128-row truth table gets solved now with a second technique, theorem proving — "5 lines and you are done," was the promise, "but it also has some drawbacks. We will look at it after we complete this." The query is again $\neg P_{1, 2}$ : can it be inferred from the knowledge base? We have the five rules $R_{1}$ to $R_{5}$ . A literal is a single atomic fact; $R_{1} = \neg P_{1, 1}$ , $R_{4} = \neg B_{1, 1}$ and $R_{5} = B_{2, 1}$ are literals standing alone. The rules with actual structure are $R_{2}$ and $R_{3}$ , and we must start from one of those — the session starts with $R_{2}$ (the reasoning is explained in 10.4.2).

Worked derivation: proving $\neg P_{1, 2}$ in six named steps.

Step 1 — Biconditional elimination on $R_{2}$ . $R_{2} = B_{1, 1} ⟺ (P_{1, 2} \lor P_{2, 1})$ matches the LHS pattern $α ⟺ β$ with $α = B_{1, 1}$ and $β = (P_{1, 2} \lor P_{2, 1})$ , so we replace it by the RHS of the biconditional elimination rule:

$R_{6} = (B_{1, 1} \Rightarrow (P_{1, 2} \lor P_{2, 1})) \land ((P_{1, 2} \lor P_{2, 1}) \Rightarrow B_{1, 1})$

We are not deleting $R_{2}$ — "you can keep that R2, but I'm adding a new rule R6, which is actually the same as R2 only" — the two are logically equivalent.

Step 2 — And-elimination on $R_{6}$ . Now $R_{6}$ is of the form $α \land β$ : one conjunct is $B_{1, 1} \Rightarrow (P_{1, 2} \lor P_{2, 1})$ , the other is $(P_{1, 2} \lor P_{2, 1}) \Rightarrow B_{1, 1}$ . And-elimination says both conjuncts are true individually. The professor picks the second one, "I am considering only beta" (you could take only the first and proceed equally):

$R_{7} = (P_{1, 2} \lor P_{2, 1}) \Rightarrow B_{1, 1}$

Step 3 — Contraposition on $R_{7}$ . $R_{7}$ has the shape $α \Rightarrow β$ with $α = (P_{1, 2} \lor P_{2, 1})$ and $β = B_{1, 1}$ . Contraposition — "if alpha implies beta is true, then negation beta implies negation alpha" — rewrites it:

$R_{8} = \neg B_{1, 1} \Rightarrow \neg (P_{1, 2} \lor P_{2, 1})$

This is the step flagged as "it's very important step" — the choice of rule here decides how many steps the proof takes.

Step 4 — Modus ponens on $R_{8}$ with $R_{4}$ . Look at $R_{8}$ : it is of the form $α \Rightarrow β$ with $α = \neg B_{1, 1}$ . Do we have $α$ directly given? Yes — $R_{4} = \neg B_{1, 1}$ is sitting in the knowledge base. That is the exact setup for modus ponens: "if alpha implies beta and if alpha are given, I can use my modus ponens and get beta." The reason for the earlier choices: "I did that because I knew already that this is given to me, and if I can bring something of this form, I can apply modus ponens." Result:

$R_{9} = \neg (P_{1, 2} \lor P_{2, 1})$

Step 5 — De Morgan's law on $R_{9}$ . The negation sits outside a disjunction: "negation is outside, I have alpha or beta inside." De Morgan's law drives the negation inside and flips the OR to an AND:

$R_{10} = \neg P_{1, 2} \land \neg P_{2, 1}$

Step 6 — And-elimination on $R_{10}$ . Both conjuncts are true individually; take $\neg P_{1, 2}$ :

$R_{11} = \neg P_{1, 2}$

Conclusion: $\neg P_{1, 2}$ is derived, so there is no pit at (1,2).

Sense-check: the final statement is exactly the query we wanted, and every intermediate line followed from the previous one by a named rule of the book — no step was a guess. Six inference steps — biconditional elimination, and-elimination, contraposition, modus ponens, De Morgan, and-elimination again — replace the 128-row table.

The summary of the whole chain: "I took my R2... I applied biconditional elimination on this... I had an AND gate... I picked this term, and I did and elimination... on this statement, I apply contraposition... I did that because I knew already that this is given to me... I could eliminate this part also and get only this as my answer. And on that, I could apply De Morgan... both are AND gate, so both of them are individually true. So I took this part and this is what was asked to me."

10.4.2 The Intuition Behind Each Step

The derivation above is intuition-driven, not mechanical, and the professor walked through the thinking move by move so the intuition can be learned:

Start with the rule that contains the query literal. The query is about $P_{1, 2}$ . Between $R_{2}$ and $R_{3}$ , choose $R_{2}$ , because it contains $P_{1, 2}$ directly, while $R_{3}$ carries $P_{3, 1}$ and $B_{2, 1}$ and more terms overall. "If you see here, this full term R3, it doesn't even have P12... I know that, okay, what I am interested in is directly available here."
Break the double implication first. Only one rule in the book matches a double implication, so until $R_{2}$ is broken into single implications, none of the other rules can touch it. "With double implication, I cannot do much... it's best for me to first break that."
Pick the and-elimination side that sets up modus ponens. From the AND gate we could take either conjunct, but taking $(P_{1, 2} \lor P_{2, 1}) \Rightarrow B_{1, 1}$ puts $B_{1, 1}$ on the right; contraposition moves it to the left, giving $\neg B_{1, 1} \Rightarrow \neg (P_{1, 2} \lor P_{2, 1})$ ; and $\neg B_{1, 1}$ is already in the KB as $R_{4}$ , so modus ponens fires. Had we picked the other conjunct, $B_{1, 1}$ would already be on the left and the setup would be lost. "Right, you could have picked this also, but here B11 is as it is, right? But here negation B11 is given. So I wanted to apply modus ponens later."
At every step ask: am I moving toward the query? "At every step, you have to think, am I going towards it right?" Each choice shrinks the statement toward $\neg P_{1, 2}$ .

Analogy — a maze with rule-shaped doors. Think of the proof as a maze: every room is a statement, and each rule opens one kind of door. The blind way is to open every door in every room — that is the truth table. The skilled way is to read the room: the query mentions P12, so head toward the room that contains P12 (R2); a double implication has only one key (biconditional elimination), so use it at once; and since you are already carrying the fact "not B11", aim every door you open at bringing "not B11" to the left of an implication, because then modus ponens can fire. Where the analogy breaks: in a maze you can see the rooms you already visited, while a proof has infinitely many derivable statements — which is exactly why the rule choice, not the room count, decides the route length.

The honest note: "you will also get this only by practice if you actually solve a lot more problems on this category," and the math textbook has plenty of them.

10.4.3 Drawbacks: Intuition, Roundabouts, and Backtracking

The technique's weakness is its freedom. If you apply the wrong rules you do not get a wrong answer — you get a long answer:

The right route needed 6 statements; a wrong route might need 15 or 20: "you will not achieve it in six steps. You will take maybe 15 steps to go there. Because at some point you will get stuck."
You are allowed to use any rule any number of times: "you are free to use any rules any number of times."
When stuck, you backtrack: "you will see, okay, by applying this implication elimination I couldn't do, let me apply contraposition and then try to see if something happens for me." An agent that does not know the target literal behaves the same way: "If it doesn't know, it will backtrack."
The stopping rule: "If you exhaust all the rules, you don't have any more new type of rules that can be generated, then only you should conclude" that the query cannot be inferred — the answer is then false. Until every rule is exhausted, you have not earned the negative conclusion.

Visualize the proof as a chain. Draw the six statements as boxes connected by arrows: $R_{2} \to R_{6} \to R_{7} \to R_{8} \to R_{9} \to R_{10} \to R_{11}$ , and label each arrow with the rule that produced it — biconditional elimination, and-elimination, contraposition, modus ponens, De Morgan, and-elimination. The chain is the proof; the arrow labels are its justification. A wrong route looks the same shape but with 15 to 20 boxes and dead-end branches, and each dead end forces a backtrack to an earlier box.

Scope: what theorem proving assumes and what it costs. The technique applies whenever the knowledge base is a set of propositional sentences — no truth table needed, and irrelevant rules can simply be ignored (the proof of $\neg P_{1, 2}$ never mentions $P_{2, 2}$ or $B_{2, 1}$ ). Its cost is not exponential rows but search: choosing the right rule at each step, and backtracking when a choice leads nowhere. The rules only ever add statements — entailments already found never get invalidated by adding more rules, a property called monotonicity. The honest comparison to the truth table: "is this better than truth table? If you have that intuition... I'll be able to apply it in five to six statements." The intuition, not the rule book, is what makes theorem proving fast.

Common traps in theorem proving:

Starting from the wrong rule. The query mentions P12, so R2 (which contains P12) is the starting point; starting from R3, which does not even contain P12, sends the proof in the wrong direction.
Not naming the rule at each line. "Names will be required, otherwise we'll not even know what we are inferring" — a proof without rule names is not a proof.
Concluding "cannot be proved" too early. The negative conclusion is earned only after every rule has been tried; a stuck route means backtrack, not give up.
Applying rules without a direction. Any rule may be used any number of times, but using them randomly produces 15–20 step proofs — the technique is only fast when each step moves toward the query.

One context note: this material was "created for theorem proving, logic detection, and symbolic logic" long before AI existed — AI inherited it.

10.4.4 Student Questions and Answers

Q: Do we finally reach the answer even if we take a different approach? A: Yes, you will still get there — but the number of steps will vary. With the right rules you finish in about six statements; with a wrong turn you may take fifteen or more steps, get stuck, and have to backtrack to try another rule. That is the whole drawback of this technique.

The next question probes the order of the rules:

Q: What if we had applied contraposition in the very first statement? A: You cannot, because the first statement is a double implication. Contraposition works on a single implication, alpha implies beta. You must first break the double implication with biconditional elimination; only after that can you apply contraposition to the pieces.

A student then asked how anyone picks the short route at all:

Q: How do we determine whether our route is the most optimal? A: That is where intuition comes in. The query was about P12, so between R2 and R3 we chose R2 because it contains P12 directly and has fewer literals, while R3 also carries P31, B21, and more terms. Then we break the double implication first because only one rule matches it. Then, from the AND gate, we take the side that puts B11 on the right of the implication, because negation B11 is already given and modus ponens can fire. This intuition comes from solving many problems.

One exchange considered a shortcut that avoids contraposition entirely:

Q: Instead of taking the implication and applying contraposition, could we take the other side of the AND, negate the whole statement, and apply modus ponens directly? A: Yes, that is also correct, and it reaches the same answer with fewer steps. Negate both sides of the implication $(P_{1, 2} \lor P_{2, 1}) \Rightarrow B_{1, 1}$ : you get $\neg B_{1, 1} \Rightarrow \neg (P_{1, 2} \lor P_{2, 1})$ . Since $\neg B_{1, 1}$ is already given as $R_{4}$ , modus ponens fires and gives the negation of P12 or P21 directly. Then the same De Morgan's law and the final split give $\neg P_{1, 2}$ . So the answer is the same, and the route is shorter.

Next came the agent's own behavior and the format of the proof:

Q: Will an agent know that it needs to consider P12? A: No. If it does not know, it will take a rule, get stuck, backtrack, and try another, until it either reaches the conclusion or exhausts all possible rules and reports that the query cannot be inferred.

Q: Will the names of the rules be required? A: Yes, names will be required — otherwise we would not even know what we are inferring at each step.

Q: While applying negation, there is nothing to change — can we directly apply negation on both sides? A: Yes, you can apply negation to the whole statement on both sides; nothing else needs to change.

Exam note: pure rule-book derivations of this kind are "school math or undergrad math" and "for an exam point of view, it's not really useful because we have moved way beyond all this" — but the equivalence rules themselves are the foundation of the resolution technique that is examined, so they matter a lot. Know each rule by name, because the examined technique (PL resolution) is built on exactly these names.

Recap: six named rules replaced 128 table rows — fast when the intuition is right, long and backtracking-heavy when it is not. Up next: a way to prove the negation of the query instead of the query itself.

10.5 Proof by Contradiction

10.5.1 Negate the Query, Assume It, Derive a Contradiction

The trick: to prove a statement true, prove that its opposite leads to nonsense. For a lot of logic-based systems, "proving the negation sometimes is quicker than going towards the true value" — and the next examined technique (PL resolution) is built directly on this idea.

Proof by contradiction is a general mathematical technique, introduced now because the next technique (PL resolution) is built on it. The recipe:

The contradiction recipe:

Take the query you want to prove — say we want to know whether $\neg P_{1, 2}$ holds.
Negate it. The negation of $\neg P_{1, 2}$ is $P_{1, 2}$ , because double negation cancels:

$\neg (\neg P_{1, 2}) \equiv P_{1, 2}$

Assume the negated query is true, and add it to the knowledge base.
Run the same theorem-proving machinery.
If the inference ultimately comes out false — we hit a contradiction — the assumption was false, so the original query was true. If the inference comes out true, the assumption was true, so the original query was false.

The everyday version: suppose the claim is "Mohan likes apples". Instead of proving it, assume the opposite — "Mohan doesn't like apples" — add that to the knowledge base, and try to derive a contradiction. If the negation leads to contradiction, the negation is false and the original claim is true.

One presentation rule attached to this: "You should not combine and so on. You should show every step what we are doing" — contradiction proofs must be written step by step, with each rule named.

Worked check: why a contradiction is a dead end. Take the statement $P_{1, 2} \land \neg P_{1, 2}$ . What is its truth value? "It is always false. Right, because if this is true, the negation, this part will become false... whatever you do, the statement is false."

Run the two cases:

If $P_{1, 2}$ is true, then $\neg P_{1, 2}$ is false, and a conjunction with one false part is false.
If $P_{1, 2}$ is false, the conjunction is false at the first part already.

Either way the statement is false — a statement and its own negation cannot both hold. So if the knowledge base plus the assumption contains a statement and its direct negation, "immediately your rule can be flagged as false" — the contradiction is instant. And then the chain does the work: inference false → assumption false → query true. "So in very quick steps, you will be able to conclude some things."

Sense-check: the contradiction tells us the assumption is false, never the query. The assumption was the negation of the query, so the query itself must be true — the double negation at the start of the recipe is exactly what makes the final step legal.

Visual intuition. Draw the refutation as a flow with four stops:

$assume \neg q \to derive a contradiction \to assumption is false \to q is true$

The arrow that matters is the last one: the contradiction only ever points back at the assumption, and the assumption is the negated query.

10.5.2 Why Contradiction Is Often Shorter

Why would anyone deliberately prove the negation instead of the statement itself? Because it is frequently shorter: "for a lot of logic based systems, proving the negation sometimes is quicker than going towards the true value." The simple demonstration: take $P_{1, 2} \land \neg P_{1, 2}$ . The statement is always false; so if the knowledge base plus the assumption contains a statement and its direct negation, a contradiction is immediate — "if you had added some rule which is contradicting to something in your knowledge base, immediately your rule can be flagged as false." And then the chain does the work: inference false → assumption false → query true. "So in very quick steps, you will be able to conclude some things." That is exactly why the next technique exists: "this is a technique which we will use later."

Scope: when contradiction is the right tool. The recipe applies to any propositional knowledge base and any query expressible in it, and it is the standard engine of refutation-based proof systems. It shines when the negation of the query clashes immediately with an existing rule — the clash is usually easier to spot than a direct proof route. It does not remove the search problem: after adding the assumption you still need some inference machinery (theorem proving, or later resolution) to find the contradiction, and if the query is not entailed you will search in vain. The technique also assumes the knowledge base is consistent — from an inconsistent KB, every query would "prove" by contradiction, which tells you nothing.

Contradiction is also one of mathematics' oldest tools: the classic proof that there are infinitely many prime numbers assumes there are only finitely many, multiplies them all, adds one, and shows the result is a prime not on the list — a contradiction, so the assumption fails and the infinitude claim holds. The same shape, in logic notation, is what the next technique automates.

Common traps in contradiction proofs:

Forgetting the double negation. The negation of $\neg P_{1, 2}$ is $P_{1, 2}$ , not $\neg P_{1, 2}$ again — negate the whole query once.
Reading the chain backwards. A contradiction makes the assumption false, which makes the query true. Students sometimes conclude "query false" — that is the opposite of the chain.
Merging steps. "You should not combine and so on" — each rule application must be shown separately with its name.
Treating the assumption as a fact. The negated query is added for the proof only; mixing it into the permanent knowledge base muddies every later query.

Recap: proof by contradiction proves $\neg P_{1, 2}$ by assuming $P_{1, 2}$ , deriving a contradiction, and concluding the assumption must be false. It is the exact engine of the next technique — PL resolution is a mechanical way to hunt for that contradiction.

10.6 Propositional Resolution with CNF

10.6.1 Conjunctive Normal Form (CNF)

The promise of this section: one single inference rule, applied mechanically, replaces all the intuition of theorem proving. But the rule only works on statements written in one special shape — conjunctive normal form — so the shape comes first.

CNF (conjunctive normal form) is a specific way of writing a propositional logic statement. A clause is whatever sits inside one pair of brackets; in the knowledge base, $R_{2}$ and $R_{3}$ are clauses, while $R_{1}, R_{4}, R_{5}$ are single literals with no internal structure. A statement is in CNF when:

every clause contains only OR gates inside it (it is a disjunction of literals), and
the clauses are joined only with AND gates (a conjunction of clauses).

CNF, the definition: "The conjunctive normal form is a conjunction of one or more clauses, where each clause is a disjunction of literals." A clause may even be a single literal standing alone — "it can be a literal also... that's okay." So the pattern is

$(literal \lor literal \lor \dots) \land (literal \lor \dots) \land \dots$

with any number of clauses and any number of literals per clause. The sandwich rule to remember: AND outside, OR inside — clauses joined by AND, literals joined by OR.

There is a dual form called disjunctive normal form, but "we will not do that. Only CNF, let's look." For the whole resolution technique to work, every statement in the knowledge base must be in CNF: "for this whole technique to work, I should first have all my statements in that form. If I don't have it in that form, I should convert it to that form." The conversion itself is a fixed four-step flowchart — the subject of section 10.7.

10.6.2 The Resolution Rule and Unit Resolution

Resolution is a single inference rule. Suppose we have two clauses $A \lor B$ and $\neg B \lor C$ . The literal $B$ appears plain in the first clause and negated in the second — such a pair is called a complementary pair of literals. Resolution says: cancel them, and whatever remains, keep:

$\frac{A \lor B , \neg B \lor C}{A \lor C}$

Why is the cancellation legal? In this domain $B$ must be either true or false — "it cannot be both. Depending on whether it is true or false, either ways B and negation B are opposites" — so one of the two clauses always contributes the other literal. Trace the two cases: if $B$ is true, then in the second clause $\neg B$ is false, so $C$ must be true for that clause to hold; if $B$ is false, then in the first clause $A$ must be true. Either way, one of $A$ or $C$ is guaranteed — which is exactly what $A \lor C$ claims. The quick example: $A \lor B$ and $\neg A$ have complementary literals, "so that gives you only B... I have cancelled these two."

The resolution rule and its class version.

Full rule (any two clauses, one complementary pair): $\frac{ℓ _{1} \lor \dots \lor ℓ _{k} , m _{1} \lor \dots \lor m _{n}}{ℓ _{1} \lor \dots \lor ℓ _{i - 1} \lor ℓ _{i + 1} \lor \dots \lor ℓ _{k} \lor m _{1} \lor \dots \lor m _{j - 1} \lor m _{j + 1} \lor \dots \lor m _{n}}$ , where $ℓ_{i}$ and $m_{j}$ are complementary.

For PL resolution we use a restricted version called unit resolution: one side of every resolution must be a unit clause — a single literal standing alone (with or without negation). "Whatever you are trying to cancel, right, one side should be only a unit literal." The general rule (both sides may be multi-literal clauses) exists, but the class technique always requires one unit side: "that's why it's called unit resolution."

Unit resolution in symbols: $\frac{ℓ _{1} \lor \dots \lor ℓ _{k} , m}{ℓ _{1} \lor \dots \lor ℓ _{i - 1} \lor ℓ _{i + 1} \lor \dots \lor ℓ _{k}}$ , where $m$ is the unit literal and $ℓ_{i}$ is its complement.

The terminology is flagged explicitly because students mix it up — "resolution and elimination are the same, but use the term resolution. That's the actual rule. Elimination, you have other like and-elimination and so on" — so say resolution for this rule, and reserve elimination for rules like and-elimination and biconditional elimination. The full rule is complete for propositional logic; the restricted unit version is the one the course uses — the professor's exact setup — so the exam problems are built so that a unit clause is always available on one side.

10.6.3 A Small Worked Example: Resolving to the Empty Set

Worked example: a tiny knowledge base, resolved to nothing.

The warm-up problem: a tiny knowledge base in CNF, with clauses

$R_{1} = A \lor B \lor \neg C, R_{2} = A \lor \neg B, R_{3} = \neg A$

and a query $\neg C$ : is it inferred from this knowledge base? (A query should always involve literals that appear in the KB — "if I give you query as D, D is not even there in my knowledge base... should not be like that." The session also mentioned a fourth single-literal clause in passing, but the chain below works with exactly the three clauses above, so that is the clause set used.)

Step 0 — prepare the clauses. First, and-elimination lets us break the big conjunction into individual clauses, each of which must be true. Then the contradiction step: negate the query and add it to the KB. The negation of $\neg C$ is $C$ , so we add the assumption

$R_{5} = C$

"I will negate my query and add it to my knowledge base... I will put C itself there... I have assumed that my C also is true."

Step 1 — resolve $R_{1}$ with $R_{5}$ . The $C$ and $\neg C$ are complementary; they cancel, leaving $A \lor B$ :

$(A \lor B \lor \neg C) + (C) ⟹ A \lor B$

"I have one, which is A or B or negation C, and this side I have C... can I cancel them? If I cancel, what do I get?"

Step 2 — resolve the result with the unit $\neg A$ :

$(A \lor B) + (\neg A) ⟹ B$

Step 3 — resolve $B$ with $R_{2} = A \lor \neg B$ . "Negation B and you know, your B got cancelled. You had only A":

$B + (A \lor \neg B) ⟹ A$

Step 4 — resolve $A$ with the unit $\neg A$ :

$A + (\neg A) ⟹ \emptyset$

Conclusion: the result is the empty set (empty clause) — "you have an empty set here." Nothing is left after the cancellation. The interpretation of that empty set was the most asked-about point of the session; it is settled in the next subsection.

Sense-check: every step used exactly one unit clause on one side, and every cancellation removed one complementary pair — nothing else was invented.

10.6.4 The Three-Part Technique and Its Interpretation

PL resolution is not one rule but three components working together, repeated several times:

The three-part technique:

Everything must be in CNF. "If it is not in CNF form, you can't even apply this technique. You have to first translate everything to CNF."
Add the negation of the query to the knowledge base (the contradiction technique).
Apply unit resolution until you reach the empty set.

The interpretation of the empty set — the step the class kept asking about — is best read from the flow that was drawn and repeated at the end of the discussion:

$empty set \Rightarrow contradiction proved \Rightarrow the assumed clause is false \Rightarrow the original query is true$

Spelled out: you assumed the negation of the query. If that assumption drags the knowledge base into a contradiction (the empty clause), the assumption cannot be true, so the negation is false — and the query itself is true. "If you are able to go till that empty set... if your assumption is true, your original query is false. So you can answer that this negation C is not a part of my knowledge base." And the simple rule offered at the end: "if you are able to get empty, then whatever was asked to you, that is true."

Reading the counter-case with care. If instead you can never reach the empty set — every unit resolution is exhausted — the session's phrasing was: "it means inference is false... your assumption is false... the original query is true." The standard reading in the textbook is different: when resolution runs out of new clauses without producing the empty clause, no contradiction was found — so the query has not been proved entailed; it may be true or false, and the technique could not decide. Both statements agree on the exam-critical point: only the empty set is the success signal. Without it, you may not claim that the query is proved.

Common traps in resolution:

Resolving without CNF. The cancellation is legal only because every clause is a pure disjunction of literals; resolution applied to a non-CNF statement is not this technique at all.
Forgetting the negated query. PL resolution always starts by adding the negation of the query to the KB — that is what turns the search for "entailed?" into a search for "contradiction?".
Reading the empty set backwards. The empty set means the assumption is false, so the query is true — never the other way around.
Calling the rule "elimination". The professor's terminology flag: this rule is resolution; elimination is a different family (and-elimination, biconditional elimination).

10.6.5 Student Questions and Answers

Exam note: PL resolution in this course always runs the same three steps — everything in CNF, the negated query added to the knowledge base, unit resolution to the empty set. The empty set is part of the answer format whenever the question asks you to prove.

Q: How do we reach from B to empty? Can you show me that rule? A: B stands alone as a unit clause. Take R2, which is A or negation B: the B and the negation B cancel, leaving only A. Then take the rule negation A and cancel it against A — and you have the empty set.

The next question checked the exact version of the rule:

Q: In the general resolution definition, neither side was a unit — so we should not apply it? A: Correct. I first showed what resolution means in general — cancel complementary literals across two clauses — but in PL resolution we use unit resolution, where one side must be a single literal standing alone. That is why it is called unit resolution.

A misconception about the empty set needed untangling:

Q: Since we are applying AND on two true parts, it should result in a true statement only — but it gave us an empty set. A: We are not applying AND here. In resolution we cancel complementary literals, one from each clause. The empty set is the result of that cancellation — the contradiction has been attained — not the result of combining two true statements.

Q: Could we run unit resolution on R1, R2, R3 without including the clause we added for the query? A: No — that is the wrong statement. The first step of PL resolution is always to negate the query and add it to the knowledge base. If you skip that, you are not doing PL resolution; the technique requires CNF, adding the negated query, and then unit resolution.

The terminology question came up as well:

Q: Resolution and elimination are the same thing, right? Which term should we use? A: Use the term resolution — that is the actual rule. Elimination refers to other rules, like and-elimination and biconditional elimination, so mixing the terms creates confusion.

Q: Empty set means the contradiction has been attained, right? A: Yes — that is an easier way to understand it. You negated the query and put it in the knowledge base; arriving at the empty clause means the contradiction has been proved, and from there the chain gives the answer about the original query.

Q: What if we are not able to apply any unit resolution and cannot get to empty? A: Then the inference is false, so the assumption is false, so the original query is true. But note: if you have no unit literals at all, you cannot apply this technique at all — you need unit clauses and CNF to proceed. (Compare the care note on this phrasing in 10.6.4.)

Q: Can we use any unit literal and any clause? Can we reuse them? A: Yes — any unit literal and any clause can be used, and you can reuse them if needed.

Q: Do we need to show the empty set in our answer? A: Yes, we need to. If the question asks you to prove, you show it. Otherwise you are just trying to move toward empty — you might reach it or you might not.

Recap: cancellation of complementary literals is the one mechanical move; reaching a contradiction is the refutation's success signal — and it only fires when the whole knowledge base was first converted to CNF. That conversion is the next section's flowchart.

10.7 Converting a Knowledge Base to CNF

10.7.1 The Four-Step Conversion Flowchart

The Wumpus knowledge base is not in CNF, because $R_{2} = B_{1, 1} ⟺ (P_{1, 2} \lor P_{2, 1})$ and $R_{3} = B_{2, 1} ⟺ (P_{1, 1} \lor P_{2, 2} \lor P_{3, 1})$ contain double implications, and after splitting, an implication with a negated head appears. "R1, no problem for me. That's just a unit. R4, no problem. R5 no problem, query also no problem. But only my R2 and R3 are problematic because they are not in CNF format, they are not a literal also."

The remedy is a fixed flowchart of four steps, applied in order to every offending statement:

The four-step conversion flowchart:

Check for biconditional (double implication). If present, eliminate it with biconditional elimination: $α ⟺ β \equiv (α \Rightarrow β) \land (β \Rightarrow α)$ .
In whatever answer you get, check for implication. If present, eliminate it with implication elimination: $α \Rightarrow β \equiv \neg α \lor β$ .
In whatever answer you get, apply De Morgan's laws where a negation is common to a whole clause: $\neg (α \lor β) \equiv \neg α \land \neg β$ and $\neg (α \land β) \equiv \neg α \lor \neg β$ .
In whatever answer you get, apply distributivity — the step that pushes an OR inside an AND — and the result is in CNF.

The summary: "Always first check if your rule has biconditional, if it is there, eliminate it; in whatever answer you get, try to check in the second step if it has implication, if it is there, eliminate it; in whatever answer you get, apply De Morgan's; in whatever answer you get after De Morgan, apply distributivity — what answer you will get will be in CNF." These are fixed rules; follow the sequence and any statement comes out in CNF.

Analogy — a cooking recipe with a fixed order. The flowchart is like a recipe where each step changes the dish and the next step reads the changed dish: "in whatever answer you get" is repeated at every step. You cannot skip ahead — distributing an AND before eliminating the implications would leave the negated head untouched — and you cannot do the steps in a different order and call it the flowchart. Where the analogy breaks: in cooking you may improvise and still eat; here each step is a logical equivalence, so only the exact sequence is guaranteed to end in CNF.

(This conversion itself is not AI-specific: "this is all not from AI angle at all. This is a concept we are doing in order to get my terms in CNF so that I can apply my PL resolution technique.")

10.7.2 Worked Conversion of R2

Worked example: $R_{2}$ into three CNF clauses.

Start converting $R_{2} = B_{1, 1} ⟺ (P_{1, 2} \lor P_{2, 1})$ .

Step 1 — biconditional elimination. Apply biconditional elimination, with $α = B_{1, 1}$ and $β = (P_{1, 2} \lor P_{2, 1})$ :

$(B_{1, 1} \Rightarrow (P_{1, 2} \lor P_{2, 1})) \land ((P_{1, 2} \lor P_{2, 1}) \Rightarrow B_{1, 1})$

Step 2 — implication elimination on both pieces. Both pieces still contain implications. The first piece gives $\neg B_{1, 1} \lor P_{1, 2} \lor P_{2, 1}$ . The second gives $\neg (P_{1, 2} \lor P_{2, 1}) \lor B_{1, 1}$ . The AND between the pieces "is always there" — it persists through every step:

$(\neg B_{1, 1} \lor P_{1, 2} \lor P_{2, 1}) \land (\neg (P_{1, 2} \lor P_{2, 1}) \lor B_{1, 1})$

Step 3 — De Morgan on the second clause only. Now check the two clauses. The first clause is already CNF — it is all ORs, "everything in that is in OR. And here I have my AND gate. Already in CNF." Is there any need for De Morgan there? "No need for De Morgan, because this negation is not common at all. This B11 has a negation. This P12, P21 don't have any negations. But here is where the problem comes. I have a negation which is common to this." The second clause has a common negation in front of a disjunction, so De Morgan applies:

$(\neg B_{1, 1} \lor P_{1, 2} \lor P_{2, 1}) \land ((\neg P_{1, 2} \land \neg P_{2, 1}) \lor B_{1, 1})$

Step 4 — distributivity. The second clause is now an OR with an AND inside the bracket — exactly the pattern distributivity handles: $α \lor (β \land γ) \equiv (α \lor β) \land (α \lor γ)$ . Here $α = B_{1, 1}$ , $β = \neg P_{1, 2}$ , $γ = \neg P_{2, 1}$ . Distributing $B_{1, 1}$ into the bracket flips the AND to an OR between the two new clauses:

$(\neg B_{1, 1} \lor P_{1, 2} \lor P_{2, 1}) \land (\neg P_{1, 2} \lor B_{1, 1}) \land (\neg P_{2, 1} \lor B_{1, 1})$

Result: $R_{2}$ in CNF — three clauses, all ORs inside, joined by ANDs.

The same route in words: "You took the first line, you applied biconditional elimination... wherever there was implies, you applied implication elimination... only the second line has a problem, like there is a common negation... so I applied De Morgan... and then, in this, after De Morgan, I have to distribute this, I have to take it inside."

Sense-check: each step applied exactly one equivalence to one offending shape, and the final statement has no $⟺$ , no $\Rightarrow$ , and no negation wider than a single literal.

One tempting mistake to avoid: after De Morgan, you could try to distribute $\neg B_{1, 1} \lor (P_{1, 2} \lor P_{2, 1})$ — but the first line is OR outside and OR inside, and distributivity requires opposite operators, so that line is already fine and must not be touched.

10.7.3 Worked Conversion of R3

Worked example: $R_{3}$ into four CNF clauses.

The same sequence cleans up $R_{3} = B_{2, 1} ⟺ (P_{1, 1} \lor P_{2, 2} \lor P_{3, 1})$ — the professor confirmed the structure: "we have done for this rule also, we have eliminated biconditional and so on" — and every intermediate line mirrors $R_{2}$ 's conversion exactly:

Step 1 — biconditional elimination:

$(B_{2, 1} \Rightarrow (P_{1, 1} \lor P_{2, 2} \lor P_{3, 1})) \land ((P_{1, 1} \lor P_{2, 2} \lor P_{3, 1}) \Rightarrow B_{2, 1})$

Step 2 — implication elimination on both pieces:

$(\neg B_{2, 1} \lor P_{1, 1} \lor P_{2, 2} \lor P_{3, 1}) \land (\neg (P_{1, 1} \lor P_{2, 2} \lor P_{3, 1}) \lor B_{2, 1})$

Step 3 — De Morgan on the second clause, where the negation is common:

$(\neg B_{2, 1} \lor P_{1, 1} \lor P_{2, 2} \lor P_{3, 1}) \land ((\neg P_{1, 1} \land \neg P_{2, 2} \land \neg P_{3, 1}) \lor B_{2, 1})$

Step 4 — distributivity of $B_{2, 1}$ over the AND inside the bracket — "similarly, here also, you could have taken inside" — giving the four clauses:

$(\neg B_{2, 1} \lor P_{1, 1} \lor P_{2, 2} \lor P_{3, 1}) \land (\neg P_{1, 1} \lor B_{2, 1}) \land (\neg P_{2, 2} \lor B_{2, 1}) \land (\neg P_{3, 1} \lor B_{2, 1})$

Result: $R_{3}$ in CNF — four clauses.

Sense-check: the pattern is identical to $R_{2}$ — one biconditional became two implications, two implications became two disjunctions, the common negation moved inside, and one distributive step turned the AND-inside-OR into three separate clauses.

The whole converted knowledge base now has no implications and no double implications anywhere: "instead of R2, R3, all these new rules have come. Do I have anywhere implication, double implication, not all that? Nothing. Everything is in CNF format now." The new clauses get fresh numbers — $R_{6}$ through $R_{12}$ — with $R_{6} = \neg B_{1, 1} \lor P_{1, 2} \lor P_{2, 1}$ , $R_{7} = \neg P_{1, 2} \lor B_{1, 1}$ , $R_{8} = \neg P_{2, 1} \lor B_{1, 1}$ from $R_{2}$ , and $R_{9} = \neg B_{2, 1} \lor P_{1, 1} \lor P_{2, 2} \lor P_{3, 1}$ , $R_{10} = \neg P_{1, 1} \lor B_{2, 1}$ , $R_{11} = \neg P_{2, 2} \lor B_{2, 1}$ , $R_{12} = \neg P_{3, 1} \lor B_{2, 1}$ from $R_{3}$ . (The numbering follows the later resolution run, which reuses $R_{4}$ , $R_{5}$ as units and adds the negated query as $R_{13}$ in section 10.8 — the scheme is consistent throughout.) Now PL resolution can run.

10.7.4 Student Questions and Answers

Q: Why is distributivity applied only to this part and not to the first line? A: Look at the distributivity rule — it applies only when the operator outside the bracket is opposite to the operator inside: OR outside with AND inside, or AND outside with OR inside. The first line is OR outside and OR inside, so the rule cannot be applied there; that line is already in CNF. Only the second line has the mixed structure, so only there do we distribute.

Q: Is this full line already in CNF format? A: Yes — everything in it is OR, and it is joined to the rest with an AND gate, so it is already in CNF and nothing changes for it.

Exam note: expect to rewrite statements into CNF as the fixed four steps — biconditional first, then implication, then De Morgan, then distributivity — in that exact order, and to name the step you are applying.

The four steps are the only moving parts here — everything else in the technique is fixed by the order.

Recap: every offending statement passes through the same four steps — eliminate biconditionals, eliminate implications, push negations in with De Morgan, distribute OR over AND. The converted Wumpus KB yields seven fresh numbered rules, R6 to R12 — and now PL resolution can finally run on the Wumpus problem itself.

10.8 PL Resolution on the Wumpus Problem

10.8.1 Add the Negated Query, Resolve, Reach Empty

Now everything is in place: the KB is in CNF (clauses $R_{1}, R_{4}, R_{5}$ as units, $R_{6}$ through $R_{12}$ as the converted clauses), and the query is again $\neg P_{1, 2}$ .

First, the contradiction step: negate the query and add it to the KB. The negation of $\neg P_{1, 2}$ is $P_{1, 2}$ , so the new assumption is

$R_{13} = P_{1, 2}$

"I should negate this and put it into my knowledge base... Negation of my query: what is that? Negation of negation P12 and what is that? Correct. Done that."

Worked example: two unit resolutions to the empty set.

Then unit resolution. The unit clauses available are $R_{1} = \neg P_{1, 1}$ , $R_{4} = \neg B_{1, 1}$ , $R_{5} = B_{2, 1}$ , and the new $R_{13} = P_{1, 2}$ . We need a unit on one side and, on the other side, a clause containing its complement. Pick $R_{4} = \neg B_{1, 1}$ and pair it with $R_{7} = \neg P_{1, 2} \lor B_{1, 1}$ , because $B_{1, 1}$ and $\neg B_{1, 1}$ are complementary — "this is R4, he is alone, and here... which rule is this? This is very good, R7." Why R7 and not R8? Both contain $B_{1, 1}$ , but cancelling with R8 would leave $\neg P_{2, 1}$ , which is not what we are chasing; cancelling with R7 leaves $\neg P_{1, 2}$ , exactly the query. "If I had picked the R8 there also I could have cancelled that B11 B11 but in output I would have got negation P21, which is not what I'm looking for. I'm looking for the query which is P12."

$R_{4} + R_{7} ⟹ \neg P_{1, 2}$

Now $\neg P_{1, 2}$ meets the assumed $R_{13} = P_{1, 2}$ — complementary literals again:

$\neg P_{1, 2} + R_{13} ⟹ \emptyset$

Result: the empty set. Two resolutions after the conversion, and the contradiction is achieved: "I have R13 here, which is P12, cancel them, you got empty. If you got empty, what does that mean? Your queries, your inference is false... If your inference is false... your assumption is false... your query is true."

Sense-check: the first cancellation was chosen deliberately — R7's remaining literal is the query itself, which is exactly what the assumed R13 can cancel against; R8 would have stranded us with $\neg P_{2, 1}$ .

One presentation rule from this example: you must show the cancellations and every step. A student asked whether one may simply write "since $\neg B_{1, 1}$ is true, $\neg P_{1, 2}$ is true" — the answer: "No, you should do this and show. You can't just write that. You should eliminate like this and cancel and show."

10.8.2 Reading the Empty Set: The Flow of Contradiction

The professor drew the flow once more, because this was the moment of maximum confusion: "There were some confusions before... on if it is an empty what it is."

The chain to memorize:

$empty set reached \Rightarrow contradiction achieved \Rightarrow inference is false \Rightarrow assumption (added clause) is false \Rightarrow original query is true$

"If this is empty, you can tell this flow chart, right? This inference is false. My assumption is false, so my given query is true." And the simple memory aid repeated for everyone: "if you are able to get empty, then whatever was asked to you, that is true." The empty set is the success signal of the refutation: the negation of the query cannot coexist with the knowledge base, so the query itself must hold.

Exam note: expect to show a resolution run end to end — conversion to CNF if needed, the negated query added, the unit resolutions one by one, and the final empty set. "If the question asks you to prove, then you will [show the empty set]" — the empty set is part of the answer format, and so are the cancelled pairs.

10.8.3 All Techniques Agree: No Pit at (1,2)

The conclusion of the resolution run is $\neg P_{1, 2}$ — no pit at (1,2) — "and that is the same result we have been getting in other techniques also, if you remember." The truth table showed $P_{1, 2}$ false in all three satisfying rows; theorem proving derived $\neg P_{1, 2}$ in six steps; resolution reaches the empty set with the assumed $P_{1, 2}$ . Three independent routes, one answer. That consistency is the reassurance that the contradiction machinery is reading the empty set correctly: "here also we were able to prove this. In theorem proving also we got that as valid and group table also we had got that right."

10.8.4 Student Questions and Answers

Q: In this clause, since it was OR and negation B11 is true, that is why we could remove B11, right? A: In resolution you are only bothered about complementary literals appearing across the two clauses — here negation B11 in one clause and B11 in the other — you cancel them. You are not bothered about the AND or OR symbols themselves. But if there had been an AND gate inside the clause instead of OR, we could not have cancelled; that is the whole point of CNF. In CNF every clause contains only OR, so the cancellation is always legal, and you cannot apply PL resolution to non-CNF statements. Also note the literals must be of opposite sign — complementary — otherwise there is nothing to cancel.

The next question traced where the assumption came from:

Q: How do we get R13? A: R13 is the negation of the query. The query is negation P12, so its negation is P12 — the double negation cancels — and we add that to the knowledge base as an assumption. Always first negate the query, put it into the rule set, and only then apply unit resolution.

The class's central doubt came up again, this time about the direction of the reading:

Q: This empty set — does it mean the added clause is true, or does it mean it is false? A: The added clause is false. The empty set means the inference is false; the inference here is the assumption we added, so the assumption is false; and if the assumption is false, the original query is true.

A student wanted the reason behind the flow itself:

Q: Why does an empty set mean the inference is false? I thought reaching empty meant the logic has been used up, so the inference is true. A: To prove something as true you should keep resolving until you have resolved every rule — resolving only to the query is not good enough, because that is the clause we assumed and put in ourselves. The opposite of that is going to empty: you cannot go further, so the inferencing is false. If the inferencing is false, your assumption was false — that is the backtracking. So in every problem your attempt is to reach the empty set; if you achieve it, the original query is true.

Q: What if we reach an empty set using some other unit resolution clause, without using the assumption we added? A: That is fine — that conclusion still stands, and the answer is still true. Any unit resolution, with or without the assumed rule, is allowed. In practice, when you go deeper into these problems, you will end up using the assumed rule anyway, because it is always a unit clause and that is usually what lets you reach empty.

Q: If both sides had been B11, would P12 be left instead of negation P12? How would we show that? A: We are only cancelling complementary literals. Here we cancelled negation B11 against B11 and were left with negation P12 alone; then the assumed P12 — our assumption — was available, so we cancelled those and got empty. If the literals had both been B11, there would be nothing complementary to cancel.

Recap: the refutation is complete: the assumed negation cannot live with the knowledge base, so the assumption is false and the original statement is true — the same answer every technique produced. The contradiction machinery and the truth table read the Wumpus world identically; the next and last technique shows how to reach those satisfying rows without any table at all.

10.9 The DPLL Algorithm

10.9.1 History and Idea: Skip the Truth Table

The final technique's audacity: the truth table wrote down all 128 rows to use 3. DPLL asks the reverse question — can we find those 3 rows without ever writing the other 125? The idea is old, the payoff is modern: the same machinery now powers industrial satisfiability solvers.

The last technique is DPLL, named for Davis, Putnam, Logemann, and Loveland. The framing: "developed by Davis, Putnam, Logeman and Loveland. They had no idea about AI. They did this in 1950s for mathematical logic. But then later now we are using that." (One remark in the session dates the idea at roughly 70 years old, consistent with a 1950s origin.)

DPLL, the definition: DPLL is a complete, backtracking-based search algorithm for deciding the satisfiability of a propositional logic formula in conjunctive normal form, with improvements such as early termination, the pure symbol heuristic, and the unit clause heuristic. "Complete" here means: if a satisfying assignment exists, the search will find one.

The motivating observation is the one from 10.2: for seven literals the truth table has $2^{7} = 128$ rows, and we cared about exactly 3 of them — the rows where every rule is true. "DPLL is suggesting you try to get that three rows directly. Don't enumerate the truth table. You try to somehow get to those three rows... so that you can directly go to the next steps." For computer science students, this connects to Boolean satisfiability: "There is a problem there called Boolean satisfiability... a beautiful concept around NP-complete and what are non-solvable problems... But this all stems from that." The satisfiability question is: find an assignment of true/false to the literals such that the whole knowledge base comes out true.

10.9.2 Pure Symbol Literals

The heuristic that drives the search is the pure symbol. Build a matrix with one row per rule (clause) and one column per literal. In each cell write the literal's truth value within that rule: plain literal → true, negated literal → false, literal absent from the rule → not available (a dash). The rule for filling cells: "Any term which is with negation, we put that false. Otherwise, we put it true." A dash is genuinely not available: "Not evaluated meaning it's not even available. So you should not substitute for true or false and so on. You should just take it as not available."

The pure symbol test: look down each column. A literal is a pure symbol if its value never flips across the rules: true in every rule where it appears (or absent), or false in every rule where it appears (or absent). "Such terms are called as pure symbolic terms, meaning they remain the same across the rules. It can be false also, no problem... But it should not be like B, for example, here it is true, here it got to false... It should not flip their values." The point of identifying them: "we will start this graph with a pure symbolic literal. You can start with any pure symbolic literal... if there are other symbols which are not pure symbolic, you should not start that problem with a non-symbolic literal."

Why is starting with a pure symbol safe? A pure symbol never flips sign, so assigning it its own sign can never make any clause false — the clause is either already satisfied or still waiting on its other literals. In the language of the truth table, a pure symbol can be fixed without discarding any satisfying row.

10.9.3 A Small DPLL Example: The A-B-C-D Knowledge Base

To see the matrix, take three clauses — this is a fresh example, not the Wumpus problem:

$R_{1} = A \lor B \lor \neg C, R_{2} = \neg B \lor A, R_{3} = C \lor D$

The literals involved are $A, B, C, D$ .

Worked example: the pure-symbol matrix for A, B, C, D.

Fill the matrix (T = true, F = false, dash = not available). In $R_{1} = A \lor B \lor \neg C$ : A is plain → T, B is plain → T, $\neg C$ is negated → F, D is absent → dash. In $R_{2} = \neg B \lor A$ : B is negated → F, A is plain → T. In $R_{3} = C \lor D$ : C is plain → T, D is plain → T:

Literal	R1	R2	R3
A	T	T	—
B	T	F	—
C	F	—	T
D	—	—	T

Check each column: $A$ is true, true, absent — never flips, pure. $D$ is absent, absent, true — never flips, pure. $B$ is true in R1 and false in R2 — flips, not pure. $C$ is false in R1 and true in R3 — flips, not pure. So the pure symbols are $A$ and $D$ , and the DPLL search would start its tree from one of them.

Sense-check: assigning $A = true$ and $D = true$ leaves $R_{1}$ satisfied at A, $R_{2}$ satisfied at A, and $R_{3}$ satisfied at D — the remaining symbols $B$ and $C$ are then free.

10.9.4 DPLL on the Wumpus Problem: The Tree Walk

Back in the Wumpus world, the converted knowledge base gives two clauses that matter here:

$R_{7} = \neg P_{1, 2} \lor B_{1, 1}, R_{8} = \neg P_{2, 1} \lor B_{1, 1}$

with three literals: $P_{1, 2}, B_{1, 1}, P_{2, 1}$ . The matrix:

Literal	R7	R8
P1,2	F	—
B1,1	T	T
P2,1	—	F

All three columns stay constant — $P_{1, 2}$ is false where present, $B_{1, 1}$ is true everywhere, $P_{2, 1}$ is false where present — so all three are pure symbols, and we may start the tree with any of them.

Worked example: the DPLL tree walk for R7 and R8.

The session starts with $P_{1, 2}$ as the root, with two branches: true and false.

Branch $P_{1, 2} = T$ . In $R_{7} = \neg P_{1, 2} \lor B_{1, 1}$ , the literal $\neg P_{1, 2}$ becomes false. Since $R_{7}$ is given as true, $B_{1, 1}$ must be true to save the clause — the phrase used: "B11 was the savior." With $B_{1, 1} = T$ , $R_{8} = \neg P_{2, 1} \lor B_{1, 1}$ is true no matter what $P_{2, 1}$ is, so $P_{2, 1}$ is a don't care.

Branch $P_{1, 2} = F$ . Now $\neg P_{1, 2}$ is true, so $R_{7}$ is true regardless of $B_{1, 1}$ — $B_{1, 1}$ is a don't care. Branch on $B_{1, 1}$ :

$B_{1, 1} = T$ : $R_{8}$ is true regardless of $P_{2, 1}$ — $P_{2, 1}$ is a don't care.
$B_{1, 1} = F$ : $R_{8} = \neg P_{2, 1} \lor F$ must still be true, so $\neg P_{2, 1}$ must be true — $P_{2, 1} = F$ .

The traversals yield the satisfying combinations (don't cares written as dashes):

P1,2	B1,1	P2,1
T	T	—
F	T	—
F	F	F

Result: three satisfying rows, and the fully determined one is $P_{1, 2}$ = false, $B_{1, 1}$ = false, $P_{2, 1}$ = false.

Sense-check against the rules: with $P_{1, 2}$ false, $B_{1, 1}$ false, $P_{2, 1}$ false, clause $R_{7} = \neg P_{1, 2} \lor B_{1, 1}$ reads true ∨ false = true, and $R_{8} = \neg P_{2, 1} \lor B_{1, 1}$ reads true ∨ false = true. Both clauses hold, as required.

(One note on the session's wording: "this will give you 2 rows" was said while walking the two root branches; the tree above yields three paths, two of which differ only in don't-care columns, and the final class discussion confirms the fully determined row $P_{1, 2}$ = false, $B_{1, 1}$ = false, $P_{2, 1}$ = false. Since a single satisfying row is enough, the count does not change the method.)

The walk-through of the interesting path: "if P12 was true... this would have gone false. If this was false, I know already that R7 is true... then what will be B11? B11 is true. He was the savior because he was true." And for the false branch: "if this value is false, negation of that false will become true, right? Then this is a don't care because I am an OR gate, right? Irrespective of that, anyway I'm going to get true."

The key contrast with the truth table: "This is the reverse logic of truth table. In truth table, you start enumerating everything, and then you try to see where all the knowledge base is true... But DPLL told, why are you enumerating everything? Directly you start with the problem, try to take pure symbols... start the tree with that and put true, false, true, false values and try to see, reverse engineer what rows will be true."

Two practical notes. You do not need to club all satisfying paths together with AND logic — "you can do that, but that's not even needed. As long as you have those rows which satisfy, that's good enough." And a single satisfying row is enough: "DPLL says even if you have one row... which has all the assignment of those literals which will give you the rules as true, that's good enough" — so during the search you prune every don't-care branch and keep only the DFS path that stays fully determined.

10.9.5 Why DPLL Is Not Directly Examined

The scope was explicit: "You'll not have questions and all that directly from here, but all I meant was, are we able to derive which rows will lead you to R7 and R8 being true?" DPLL in this course is a concept — the idea that satisfiable rows can be found by search rather than enumeration — not a required computation.

Exam note: do not expect a DPLL question; expect the conceptual understanding — what a pure symbol is, why the search starts with one, what a don't care is, and how the tree reaches the satisfying rows without the full table.

10.9.6 Student Questions and Answers

Q: What is a symbolic literal? If a literal is not evaluated in a rule, do we assume it follows the trend of the other rules? A: No — there is no trend to follow. If the literal is not available in that rule, leave it as a dash; do not substitute true or false for it. Not available is fine for us.

Another question was about the matrix itself:

Q: After creating the matrix, what do we derive from it? A: We look down every column. A literal whose value never flips across the rules — true stays true, false stays false, or the literal is simply absent from a rule — is a pure symbol literal. Here all three literals are pure symbols, so any of them is a valid starting point.

How the starting symbol is chosen came up next:

Q: How do we decide to start the tree with P12? A: You can start with any pure symbol literal. Here all three literals are pure symbols, so P12 is one valid choice; in any problem you may start with any pure symbol, but you should not start the tree with a non-pure literal.

The tree itself was questioned next:

Q: From the tree, how do we form the final table for P12 and B11? How many values do we consider? A: You can ignore the don't care entries — you do not explore those nodes at all. On the remaining branch you do a DFS and you get one row, and that is good enough: DPLL says even one complete assignment that makes the rules true is enough. In the B11-true case, P21 is a don't care, so you write only the determined values — the final path fixes P12, B11, and P21.

The don't-care handling raised one more doubt:

Q: In the don't care case, do we need to write both true and false? A: No — just put a dash. Don't care means the clause is already satisfied, so either value works and neither needs to be explored.

Q: What if multiple rules are involved? A: You have to check all of them. Every rule in the knowledge base must come out true; you cannot satisfy one clause and ignore the rest.

Q: How do you compare K-maps to DPLL in an AI context? A: DPLL is a very generic satisfiability tool: given a rule, how should the truth values be assigned so that the rule is true. A Karnaugh map is very different — it is not the same kind of tool at all.

Recap: DPLL is the truth table turned inside out — pick a pure symbol, branch on it, propagate the forced values, mark the don't cares, and stop at the first fully determined satisfying row. That single row is all the agent needs; the technique list for propositional logic is now complete.

10.10 The Practice Problem: From English to Contradiction

10.10.1 The Worded Exercise

To close the module's technique list, a full-chain practice problem was given: a set of worded English statements, the kind that must be translated into propositional logic before anything else can happen. The statements involve online shopping, customer-friendliness, and customers who follow tech trends and will receive something — the exact content was read out briefly and garbled in places, but the shape of the exercise is what matters: translate, convert, assign, prove. One sentence contains "not all", and the professor paused on it: how do you represent "not all" in propositional logic? — a hint that the translation step itself needs care with such quantifier-flavored phrases.

The "not all" trap. A sentence like "not all customers who follow tech trends will receive a gift" does not translate into a single propositional literal, because it talks about a group: it claims that at least one trend-following customer receives nothing. In propositional logic every customer's property is a separate fact — "customer A receives a gift" is one proposition, "customer B receives a gift" another — and the claim "not all" wants to range over the whole group at once. That is exactly the boundary where propositional logic stops and the quantifiers of the next section begin; for this exercise, the practical lesson is to notice such phrases and decide explicitly what each of them becomes in logic.

The exercise has four stages, and every stage is a technique from today:

The full-chain exercise:

Represent the knowledge base in propositional logic. Sentences like "if something happens, then..." become implications; each statement becomes a rule.
Convert everything to CNF using the four-step flowchart. "Not all rules might be in CNF," so this stage is guaranteed to be needed.
Find one complete binary satisfiability assignment — the DPLL-style question: show the value of each literal so that all the rules come out true at once.
Prove a given query by contradiction using PL resolution. Write the query in logic, negate it, add it to the knowledge base (everything is already in CNF because of stage 2), apply unit resolution, and if you reach the final empty set, the query was true.

"Instead of this PL resolution, I could have told you to do truth table. I could have told you theorem proving whatever, right? But this type of problems you can practice."

10.10.2 What to Practice for the Exam

Exam note: "These type of problems you can expect in the exam" — a worded problem solved through the full chain: propositional logic → CNF → satisfying assignment → contradiction via resolution. The four stages above are the exact shape of the expected answer.

The professor's guidance around the exercise:

Solutions to the practice problems will not be posted immediately; the expectation is that you solve them first and put your work in the discussion, after which the answers can be released. "I want you to solve it. I want you to put it in the discussion, and then maybe I will release the answers."
The math textbook mentioned earlier has many theorem-proving examples in the same style — "you can keep practicing" with it.
The logic webinar from the past week is directly useful here: it covered propositional logic with small examples and helps with the assignment too.

Pitfalls when practicing the chain:

Skipping the translation step. The worded sentences are the real input; assigning letters and writing implications is half the marks, and a wrong implication poisons every later stage.
Converting only what looks "hard". Stage 2 says every rule must end in CNF — check even the unit-looking sentences, because "not all rules might be in CNF."
Forgetting what stage 3 asks. It wants one complete binary assignment that satisfies all rules — not a truth table, not a proof — so a DPLL-style walk that lands on one fully determined row is the target.
Dropping the contradiction step in stage 4. Negate the query, add it, unit-resolve, show the empty set — the proof is the whole chain, not just the final line.

Recap: the practice problem is the module in miniature — English becomes logic, logic becomes CNF, an assignment shows satisfiability, and a resolution refutation proves the query. Solving it end to end by hand is the single best preparation for the examined version of everything in this session.

10.11 Why Propositional Logic Is Not Enough

10.11.1 "Some" and "All" Escape Propositional Logic

The module's closing question: propositional logic handled pits, breezes, and queries — but what happens when a statement talks about groups? "Some students are brilliant." "All women are beautiful." Try to write either one with only literals and connectives, and the answer comes back: you cannot.

The module closes with the question that motivates the next session: why is propositional logic not good enough? The demonstration is quick and famous. Try to say "some students are brilliant" in propositional logic. The problem word is "some" — propositional logic has no way to say that a property holds for an unspecified portion of a group. Try "all women are beautiful" — the word "all" is just as inexpressible. "How do you represent this all?" The professor's summary: "propositional logic is not good enough. That is why we will learn next class called predicate logic, where there are symbols like... that will be used to depict this all, some, few, and so on."

10.11.2 Predicate Logic Preview: Quantifiers, Forward and Backward Chaining

Everything else about the machinery stays the same: "everything else, whatever we learn today, exactly is the same. You can do that with predicate logic also." What changes is the expressive power — predicate logic adds quantifier symbols such as the universal quantifier $\forall$ (read "for all", the "all" symbol) and the existential quantifier $\exists$ (read "there exists" or "for some", the "some" symbol), so statements about groups become expressible.

The two quantifiers:

$\forall x P (x)$ — universal quantifier: $P$ holds for every object $x$ . This expresses "all": $\forall x (Brilliant (x))$ would say everyone is brilliant.
$\exists x P (x)$ — existential quantifier: $P$ holds for at least one object $x$ . This expresses "some": $\exists x (Brilliant (x))$ says at least one person is brilliant.

With these two symbols, the group statements that defeated propositional logic are written directly — which is exactly why the next session starts with predicate logic.

The technique list shrinks, though: for propositional logic we learned five techniques (truth table, theorem proving, contradiction, PL resolution with CNF, and DPLL); for predicate logic there are only two — forward chaining and backward chaining — "that's it. And that will complete our full module." The next session is expected to finish this module quickly (about an hour), and then the course moves to the multi-agent module.

Exam note: all chapters 1 to 16 are covered for the final exam; the later chapters (9 to 16) are more closely knit, and topics like games reappear in the multi-agent context, so nothing should be treated as mutually exclusive.

Q: Are chapters 9 to 16 mutually exclusive? If not, could you guide me? A: All chapters 1 to 16 are covered for the final exam. They are related, and chapters 9 to 16 are more closely knit, but chapters 1 to 8 connect too — for example, games were covered earlier, and we return to games in the next module, but in the context of multi-agent. So do not think of them as mutually exclusive; they are all related.

Recap: group statements like "all" and "some" are beyond the five techniques of this session; quantifiers are the missing piece, and the module finishes with two inference methods built on them.

Exam Guidance Summary

Everything exam-relevant from this session, consolidated:

Open book exam. The rule book (all the logical equivalences and inference rules) is available during the exam; nothing needs to be memorized from the rule book itself.
Rule names are required. Every step of a proof must name the rule that justifies it ("names will be required, otherwise we'll not even know what we are inferring").
Expect worded problems run through the full chain: translate English statements into propositional logic → convert to CNF → find one complete binary satisfying assignment → prove a query by contradiction using PL resolution (negate the query, add it to the KB, unit-resolve to the empty set). "These type of problems you can expect in the exam."
Show every step. Contradiction proofs and resolution runs must be written out: "You should show every step what we are doing." Show the empty set when the question asks you to prove — it is part of the answer format. Do not skip to conclusions ("you can't just write that").
Pure theorem proving per se is not examined — it was called "school math or undergrad math" and "for an exam point of view, it's not really useful because we have moved way beyond all this" — but its rule book is the foundation of PL resolution, which is examined.
DPLL is conceptual only. "You'll not have questions and all that directly from here" — understand the idea (find satisfying rows by search, pure symbols, don't cares) but do not expect a direct DPLL computation question.
Chapter coverage: all chapters 1 to 16 are covered for the final exam; chapters 9 to 16 are closely knit and topics recur across modules (games in the multi-agent context), so study them as related, not exclusive.
Mark structure for the course: the final component (EC3) carries 40 marks with a heavier numerical weightage ("for EC3, numerical weightage is more"); EC2 (mid-semester) is done at 13 marks; quiz 1 and quiz 2 are best-of, so a missed quiz 1 can be recovered in quiz 2; assignment 2 and quiz 2 are still pending. If the mid-semester did not go well, the remaining components still leave a lot of marks on the table.
Practice resources: the exercise problem given at the end of this session (worded problem through the full chain); the pure mathematics textbook's theorem-proving problems; and the logic webinar material, which also helps with the assignment. Solutions to practice problems will be released after discussion, not immediately.

The single most useful habit for this exam: for every proof-style question, write the five-rule Wumpus-style setup down in logic first, then apply the four-step CNF conversion, then the three-part resolution pattern — negate the query, add it, unit-resolve — and finish with the empty set. The whole session, in one routine.

Key Industry Applications

Real-world connections mentioned across the session, consolidated:

Knowledge-based agents and the Wumpus world are the classic demonstration of knowledge representation and inference in AI — the agent that incrementally builds its knowledge base from query answers is the pattern behind modern reasoning systems. "Modern AI does it in different ways, but it all boils down to this" — inferencing from a set of rules.
Truth table inferencing does not scale. Real-world use cases have so many literals that the truth table "will just explode" — the exponential $2^{n}$ growth is the practical reason theorem proving, resolution, and DPLL-style search exist.
Boolean satisfiability and NP-complete problems are the theoretical home of this material: the satisfiability question (find an assignment of literals that makes the whole knowledge base true) is the famous NP-complete problem, and DPLL is a descendant of the same idea. "This all stems from that."
DPLL and modern solvers. The algorithm was created in the 1950s for mathematical logic, "but then later now we are using that" in AI — the same backtracking-search machinery powers modern SAT-solver technology under the hood. Industrial solvers built on this line of work verify hardware circuits, check security protocols, and schedule resources in systems with tens of millions of variables.
Symbolic logic heritage. The equivalence rules and resolution were "created for theorem proving, logic detection, and symbolic logic" decades before AI adopted them — the whole technique family is inherited from mathematics, not invented for AI.
Vector databases for knowledge storage. Asked whether there are better databases than plain stores for all these static facts and actions: yes — there are more AI-specific options such as vector databases.
K-map versus DPLL. A Karnaugh map and DPLL are different kinds of tools: DPLL is a generic satisfiability algorithm (how to assign literals so a rule is true), while K-map is a very different, manual technique — not the same kind of tool at all.

ACI Lecture 10 notes · Inference Techniques in Propositional Logic

Artificial Computational Intelligence· postgraduate· 2026-08-13

Sections Breakdown

1Knowledge-Based Agents and the Inference Problem

A knowledge-based agent answers queries by checking entailment: whether every truth assignment that satisfies the knowledge base also makes the query true. The Wumpus world supplies a five-rule KB (R1-R5, seven literals) whose running query is negation P1,2, motivating a ladder of five inference techniques.

2Truth Table Inferencing

Truth table inferencing enumerates all 2^n assignments of the KB's literals, keeps the rows where every rule is true, and checks the query only there. For seven Wumpus literals the table has 128 rows of which only 3 satisfy the KB, and the query negation P1,2 is true in all three, so it is entailed; the cost is exponential.

3Logical Equivalences and Inference Rules

The rule book of logical equivalences (double negation, De Morgan, commutativity, associativity, biconditional and implication elimination, contraposition) plus the two extraction rules modus ponens and and-elimination form the toolset of theorem proving. Every equivalence is interchangeable because the two sides share the same truth table.

4Theorem Proving by Logical Inference

Theorem proving derives the query by applying named inference rules to the KB: biconditional elimination on R2, and-elimination, contraposition, modus ponens with the given negation B1,1, De Morgan, and and-elimination again yield negation P1,2 in six steps. The route needs intuition, and wrong choices cause long proofs with backtracking.

5Proof by Contradiction

To prove a query, negate it, add the negation to the knowledge base as an assumption, and derive a contradiction; the contradiction shows the assumption is false, so the query is true. A statement and its negation cannot both hold, which makes this route often shorter than direct proof.

6Propositional Resolution with CNF

PL resolution needs CNF (conjunction of clauses, each a disjunction of literals), adds the negated query to the knowledge base, and applies unit resolution until complementary literals cancel to the empty set, which proves the assumption false and the query true. The small clause set (A or B or not C), (A or not B), not A resolves to empty after adding C.

7Converting a Knowledge Base to CNF

A fixed four-step flowchart converts any statement to CNF: eliminate biconditionals, eliminate implications, apply De Morgan where a negation is common, then distribute OR over AND. R2 becomes three clauses and R3 becomes four, numbered R6 through R12.

8PL Resolution on the Wumpus Problem

With the KB in CNF (R6-R12) the query negation P1,2 is added as R13; resolving unit negation B1,1 with R7 leaves negation P1,2, which resolves with R13 to the empty set. The empty set is the success signal: contradiction achieved, assumption false, original query true. All three techniques agree there is no pit at (1,2).

9The DPLL Algorithm

DPLL (Davis, Putnam, Logemann, Loveland) is a complete backtracking search for satisfiability that skips the truth table: it finds pure symbols (literals whose sign never flips across clauses), branches a tree from one, propagates forced values, marks don't cares, and stops at one fully determined satisfying row. It is conceptual only for the exam.

10The Practice Problem: From English to Contradiction

A worded English exercise (online shopping, customer-friendly statements, customers who follow tech trends) is solved through four stages: translate to propositional logic, convert to CNF with the four-step flowchart, find one complete binary satisfying assignment, and prove a query by contradiction with PL resolution. The 'not all' phrasing needs special care in translation.

11Why Propositional Logic Is Not Enough

Propositional logic cannot express group statements like 'some students are brilliant' or 'all women are beautiful'; predicate logic adds the universal quantifier for all and the existential quantifier for some. The technique list shrinks from five propositional techniques to two for predicate logic: forward chaining and backward chaining.

12Exam Guidance Summary

Consolidated exam guidance: open book rule book, rule names required in every proof step, worded problems through the full chain (logic, CNF, satisfying assignment, resolution to empty), show every step, pure theorem proving not directly examined, DPLL conceptual only, chapters 1-16 covered, and the course mark structure.

13Key Industry Applications

Consolidated industry connections: knowledge-based agents as the pattern behind reasoning systems, exponential truth tables as the practical driver of better techniques, SAT and NP-completeness as the theoretical home, DPLL behind modern SAT solvers, symbolic logic heritage, vector databases for knowledge storage, and the K-map versus DPLL distinction.

Postgraduate students in Artificial Intelligence

Exam Revision Notes

Below is the distilled, exam-ready core. Every entry comes from the full explanation above. Use this section for rapid review; return to the main notes when a point needs more context.

Knowledge-Based Agents and the Inference Problem

Must-know: Entailment: KB entails alpha iff every assignment making all KB rules true also makes the query true; the KB grows as each query answer is added back.

$KB ⊨ α ⟺ M (KB) \subseteq M (α)$

⚠️ Top pitfall: Treating OR as 'exactly one' and reading 'iff' as a single direction; both corrupt the Wumpus rules.

Self-check: Why can we not write the Wumpus rules in plain English? The agent must evaluate and deduce mechanically, so a standard logical notation is required.

Connects to: 10.2

Truth Table Inferencing

Must-know: The truth table procedure: list all literals, draw 2^n rows, AND the rule columns, keep only rows where the whole KB is true, and evaluate the query only in those rows.

$2^{n} rows for n literals$

⚠️ Top pitfall: Checking the query in all 128 rows instead of only the 3 rows where the knowledge base is true.

Self-check: Why did the truth table need 128 rows for the Wumpus KB? Seven literals give 2^7 = 128 combinations.

Connects to: 10.1, 10.9

Logical Equivalences and Inference Rules

Must-know: Every logical equivalence has matching truth tables on both sides; modus ponens extracts beta from alpha implies beta plus alpha; and-elimination extracts either conjunct of a conjunction; each proof step must name its rule.

$\frac{α \Rightarrow β α}{β} (modus ponens), \frac{α \land β}{α} (and-elimination)$

⚠️ Top pitfall: Running rules in the wrong direction (modus ponens cannot be reversed) and confusing the equivalence symbol (equiv) with the biconditional connective (iff).

Self-check: Why is double negation an equivalence and not an inference rule? It is a two-way rewrite: both sides are true in the same models, so either may replace the other.

Connects to: 10.4, 10.7

Theorem Proving by Logical Inference

Must-know: The six-step chain R2 -> R6 -> R7 -> R8 -> R9 -> R10 -> R11 with the rule named at every step; the negative conclusion requires exhausting every rule, and rule names must be written in the proof.

$R_{7} = (P_{1, 2} \lor P_{2, 1}) \Rightarrow B_{1, 1}, R_{8} = \neg B_{1, 1} \Rightarrow \neg (P_{1, 2} \lor P_{2, 1}), R_{11} = \neg P_{1, 2}$

⚠️ Top pitfall: Applying contraposition before breaking the double implication; contraposition needs a single implication.

Self-check: Why was R2 chosen over R3 as the starting rule? Because R2 contains the query literal P12 directly while R3 does not.

Connects to: 10.3, 10.5, 10.8

Proof by Contradiction

Must-know: The chain: assume negated query, derive contradiction, assumption false, original query true; every step shown and named; negation of neg P1,2 is P1,2.

$\neg (\neg α) \equiv α, P \land \neg P \equiv False$

⚠️ Top pitfall: Concluding that a contradiction makes the query false; the contradiction makes the assumption false, so the query is true.

Self-check: What is the negation of the query negation P1,2? It is P1,2, by double negation.

Connects to: 10.4, 10.6, 10.8

Propositional Resolution with CNF

Must-know: The three-part technique: CNF everywhere, negate the query and add it, unit resolution to the empty set. Empty set means the added assumption is false, so the original query is true.

$\frac{A \lor B , \neg B \lor C}{A \lor C}, A + (\neg A) ⟹ \emptyset$

⚠️ Top pitfall: Reading the empty set as 'query false' — the empty set makes the assumption false, hence the query true; and skipping the negated-query step is not PL resolution.

Self-check: Why must every clause contain only OR gates? Resolution cancels complementary literals across clauses, and cancellation is legal only inside a disjunction.

Connects to: 10.5, 10.7, 10.8

Converting a Knowledge Base to CNF

Must-know: The four steps in order: biconditional elimination, implication elimination, De Morgan, distributivity; distributivity needs opposite operators outside and inside the bracket.

$B_{1, 1} ⟺ (P_{1, 2} \lor P_{2, 1}) \equiv (\neg B_{1, 1} \lor P_{1, 2} \lor P_{2, 1}) \land (\neg P_{1, 2} \lor B_{1, 1}) \land (\neg P_{2, 1} \lor B_{1, 1})$

⚠️ Top pitfall: Applying distributivity when both operators are the same (OR outside and OR inside); the rule requires opposite operators.

Self-check: Why is no De Morgan step needed on the first clause of R2's conversion? Because the negation is not common to the whole clause — only B1,1 is negated, not the whole disjunction.

Connects to: 10.3, 10.6, 10.8

PL Resolution on the Wumpus Problem

Must-know: The full run: negate the query to R13, unit-resolve R4 with R7 to negation P1,2, resolve with R13 to the empty set; empty set means assumption false so query true; show every cancelled pair.

$R_{4} + R_{7} ⟹ \neg P_{1, 2}, \neg P_{1, 2} + R_{13} ⟹ \emptyset$

⚠️ Top pitfall: Reading the empty set as 'the added clause is true'; it is false, and therefore the original query is true.

Self-check: Why pair R4 with R7 and not R8? Cancelling with R8 would leave negation P2,1; R7 leaves negation P1,2, exactly the query.

Connects to: 10.2, 10.4, 10.6, 10.7

The DPLL Algorithm

Must-know: A pure symbol never flips sign across clauses; start the search tree with any pure symbol; a dash means not available, never true or false; don't-care branches are pruned; one fully determined satisfying row is enough.

$R_{7} = \neg P_{1, 2} \lor B_{1, 1}, R_{8} = \neg P_{2, 1} \lor B_{1, 1}$

⚠️ Top pitfall: Substituting true or false for a dash; a literal absent from a clause is not available and stays a dash.

Self-check: Why can the tree start with any of P12, B11, P21? All three are pure symbols — each keeps one sign across both clauses.

Connects to: 10.2, 10.6, 10.7

The Practice Problem: From English to Contradiction

Must-know: Worded problems expect the full chain: propositional logic representation, CNF conversion, one satisfying assignment, then contradiction via resolution; solutions are released only after students post their work in discussion.

⚠️ Top pitfall: Translating 'not all' as a single propositional literal; group-quantified phrasing is where propositional logic stops and predicate logic begins.

Self-check: What four stages does the practice problem require? Represent in logic, convert to CNF, find one satisfying assignment, prove the query by contradiction via resolution.

Connects to: 10.1, 10.6, 10.7, 10.8, 10.9, 10.11

Why Propositional Logic Is Not Enough

Must-know: Some and all are inexpressible in propositional logic; the universal quantifier for all and existential quantifier for some restore that power; predicate logic uses forward and backward chaining instead of the five propositional techniques; chapters 1-16 all covered for the final exam.

$\forall x P (x) (for all), \exists x P (x) (there exists / for some)$

⚠️ Top pitfall: Treating chapters 9 to 16 as mutually exclusive topics; they are closely knit and topics like games recur in the multi-agent module.

Self-check: Which symbol expresses 'some'? The existential quantifier, exists x P(x).

Connects to: 10.1, 10.6, 9.x

Exam Guidance Summary

Must-know: The full-chain routine: worded problem to propositional logic, CNF conversion, one satisfying assignment, resolution with negated query to the empty set; rule names at every step; empty set shown as part of the answer.

⚠️ Top pitfall: Treating chapters as mutually exclusive; they are related and 9-16 are closely knit, with games recurring in the multi-agent module.

Self-check: What mark structure remains after the mid-semester? EC3 carries 40 marks with heavier numerical weightage, quizzes are best-of, and assignment 2 plus quiz 2 are pending.

Connects to: 10.1, 10.2, 10.4, 10.6, 10.8, 10.10

Key Industry Applications

Must-know: Inference from rules is the core of reasoning systems; satisfiability is NP-complete; DPLL-style backtracking powers modern SAT solvers in hardware verification and protocol checking.

⚠️ Top pitfall: Treating a Karnaugh map as a satisfiability algorithm; it is a manual simplification tool, not a generic assignment search.

Self-check: Why did the truth table approach fail on real-world knowledge bases? Every added literal doubles the rows, so exponential growth makes enumeration impractical.

Connects to: 10.1, 10.2, 10.9

Previous LectureLecture 09 · Knowledge Representation Using Logics

Next LectureLecture 11 · First Order Logic, Forward Chaining, and Backward Chaining

Was this lecture useful?

Loading comments…

🤖

BitsNotes AI Assistant

Subject Notes Assistant

Configure AI Chat

Choose how to access the chatbot

Have your own API key?

Switch to "Bring Your Own Key" tab above for unlimited access with any OpenAI-compatible provider.

AI Provider Preset

API Endpoint URL (OpenAI-Compatible)

API Key

Model Name

🔑 Enter API key above to fetch live models from provider, or enter model name manually.

Remember key for this session (until tab closes)

OpenAI-Compatible API Support

Choose any provider preset (Gemini, DeepSeek, Kimi, GLM, MiniMax, Qwen, OpenAI, Groq, Ollama, etc.) or enter a custom endpoint URL.

Security & Privacy First

Your API key is sent directly from your browser to your specified provider. BitsNotes servers never store or see your key.

Prerequisite Knowledge

Previously Covered in This Subject

10.1 Knowledge-Based Agents and the Inference Problem

10.1.1 The Knowledge Base and the Query

10.1.2 The Wumpus World Problem Setup

10.1.3 Why We Need More Than One Technique

10.2 Truth Table Inferencing

10.2.1 The 128-Row Truth Table

10.2.2 Exponential Cost and When It Fails

10.2.3 Student Questions and Answers

10.3 Logical Equivalences and Inference Rules

10.3.1 The Rule Book

10.3.2 Modus Ponens and And-Elimination in Plain Words

10.3.3 How the Rules Connect to the Exam

10.4 Theorem Proving by Logical Inference

10.4.1 The Worked Derivation: From R2 to R11

10.4.2 The Intuition Behind Each Step

10.4.3 Drawbacks: Intuition, Roundabouts, and Backtracking

10.4.4 Student Questions and Answers

10.5 Proof by Contradiction

10.5.1 Negate the Query, Assume It, Derive a Contradiction

10.5.2 Why Contradiction Is Often Shorter

10.6 Propositional Resolution with CNF

10.6.1 Conjunctive Normal Form (CNF)

10.6.2 The Resolution Rule and Unit Resolution

10.6.3 A Small Worked Example: Resolving to the Empty Set

10.6.4 The Three-Part Technique and Its Interpretation

10.6.5 Student Questions and Answers

10.7 Converting a Knowledge Base to CNF

10.7.1 The Four-Step Conversion Flowchart

10.7.2 Worked Conversion of R2

10.7.3 Worked Conversion of R3

10.7.4 Student Questions and Answers

10.8 PL Resolution on the Wumpus Problem

10.8.1 Add the Negated Query, Resolve, Reach Empty

10.8.2 Reading the Empty Set: The Flow of Contradiction

10.8.3 All Techniques Agree: No Pit at (1,2)

10.8.4 Student Questions and Answers

10.9 The DPLL Algorithm

10.9.1 History and Idea: Skip the Truth Table

10.9.2 Pure Symbol Literals

10.9.3 A Small DPLL Example: The A-B-C-D Knowledge Base

10.9.4 DPLL on the Wumpus Problem: The Tree Walk

10.9.5 Why DPLL Is Not Directly Examined

10.9.6 Student Questions and Answers

10.10 The Practice Problem: From English to Contradiction

10.10.1 The Worded Exercise

10.10.2 What to Practice for the Exam

10.11 Why Propositional Logic Is Not Enough

10.11.1 "Some" and "All" Escape Propositional Logic

10.11.2 Predicate Logic Preview: Quantifiers, Forward and Backward Chaining

Exam Guidance Summary

Key Industry Applications

ACI Lecture 10 notes · Inference Techniques in Propositional Logic

Sections Breakdown

Exam Revision Notes

Knowledge-Based Agents and the Inference Problem

Truth Table Inferencing

Logical Equivalences and Inference Rules

Theorem Proving by Logical Inference

Proof by Contradiction

Propositional Resolution with CNF

Converting a Knowledge Base to CNF

PL Resolution on the Wumpus Problem

The DPLL Algorithm

The Practice Problem: From English to Contradiction

Why Propositional Logic Is Not Enough

Exam Guidance Summary

Key Industry Applications

Was this lecture useful?

BitsNotes AI Assistant

Configure AI Chat

Sign in to use AI Chat