Knowledge written as logic, entailment turned into a satisfiability test, conjunctive normal form, the DPLL search, forward-rule theorem proving, and first-order logic with its quantifier scope.
Printed copy: every hidden answer below is revealed and the correct quick-check option is outlined. On screen they are hidden behind a click, which is how you should use them first.
the theory exam... tests both for factual knowledge as well as for synthetic knowledge... we also want to see that you can uh bring things across different chapters uh together because as you know by now uh the course is largely incremental.(Lecturer, T9). The four links above are examinable content, not decoration. This Part is where the CSP machinery of Part 6 comes back wearing a logician's vocabulary.
Deck p.3 draws four boxes and three arrows. You start with "Some practical problem". You encode it in a formalism. A solver that takes that formalism as input produces a solution in the formalism's own terms. You decode that back into a solution to the original problem. The whole of this Part and the whole of Part 11 are instances of that diagram.
Deck p.4 lists the instances by name: a CSP with a CSP solver, CNF (conjunctive normal form) with a SAT (satisfiability) solver, STRIPS with a planning solver and the note "(next lecture)", first-order logic with a Prolog solver, mixed integer programming with a MIP solver. It then instantiates the diagram with map colouring: the encoding is a CSP, the solver "does backtracking with AC3 and value/var heuristics", the solver's solution is the assignment WA=1, NT=2, SA=3, Q=1, NSW=2, V=1, T=3, and the decoding turns those numbers back into colours.
Of the four stages on this slide, exactly one is work that you, the modeller, must do for every new problem, and one is work that somebody did once and everybody reuses. Name both, and say which one the exercise exam actually tests.
Yours: encode (and its mirror image, decode). Reused: the solver. Deck p.5 states the reuse argument directly, that the approach often outperforms custom algorithms "because of engineering effort, if problem fits formalism well".
The exercise exam tests the encoding. Exercise session 7 asks you to translate English into propositional logic, then into CNF, and only then to run DPLL; the 2023 sample exercise exam question 5 asks for translation into first-order logic. You are never asked to build a solver.
The solver box on this slide names three techniques from Part 6 in one line. Name them, and then say what the decode step actually does here, given that the solver returned WA=1, NT=2, SA=3, Q=1, NSW=2, V=1, T=3.
Backtracking search, AC-3 (arc consistency), and value and variable ordering heuristics (the MRV, degree and least-constraining-value family). All three are Part 6 material, reused here unchanged.
Decode maps the integers back to colours: 1, 2 and 3 are names the solver invented for red, green and blue. The solver never knew it was colouring a map. That is the point of the pipeline: the formalism strips the problem down to something a general engine can chew, and the meaning is put back afterwards.
This slide gives two conditions under which the pipeline is "Very effective". State both. Then name the failure mode that the second condition is guarding against.
(1) The solver is highly optimized. (2) The encoding and decoding to the formalism is efficient, "e.g. polynomial time".
The failure mode is an encoding blow-up: if translating your problem into the formalism costs exponential time or produces an exponentially large formalism, you have paid back all the speed the solver bought you. Deck p.30 shows the same trade-off from the other side, in expressive power: the rules of chess need 100,000 pages in propositional logic and one page in first-order logic.
Deck p.5 closes with the two questions the lecture answers: "1. What formalism to encode our problem knowledge into? 2. How does the solver work?" Sections 3 to 8 below answer the first for propositional logic, sections 9 to 11 answer the second, and sections 12 to 15 answer the first again for first-order logic.
dependent on how you defined each of these aspects, how you formulated the problem, the problem will be easier or will be harder to solve. And that's something very important to realize.(Lecturer, T1, restated in T2). Said about search problems in Part 3. It transfers to this Part with no changes: the same English sentence has several correct translations into logic, and the one you pick decides how many clauses the solver sees.
Deck p.6 lists what an agent can know: the effects of actions (the transition model, from Part 3), how the world affects sensors (the sensor model), the current state of the world. Knowing these lets an agent track a partially observable world and formulate plans, which is the bridge into Part 11.
Deck p.7 gives the definition this Part is built on:
and the declarative discipline that goes with it: Tell the system what it needs to know (or have it learn the knowledge), then Ask it what to do, and the answers should follow from the knowledge base. The slide's diagram splits the system in two: the knowledge base holds "Domain-specific facts", the inference engine is "Generic code". The last bullet is the payoff and the reason this Part is abstract: "A single inference algorithm can answer any answerable question".
The slide also introduces the knowledge level as a level of description: agents can be viewed in terms of what they know, "regardless of how implemented". That is the same abstraction the pipeline of section 1 sells. Two agents with the same knowledge base are the same agent at this level, whatever their code looks like.
Deck p.8, repeated verbatim as p.11, is the frame for everything else. A logic is two things:
The picture on the slide has a left column labelled Syntaxland holding three sentences and a right column labelled Semanticsland holding a field of worlds, with arrows from each sentence to the set of worlds in which it is true. That mapping, from a sentence to its set of worlds, is the whole of semantics. Everything in section 5 (entailment) is a statement about how those sets sit inside one another.
For propositional logic this slide gives a possible world as [P=true,Q=true,R=false,S=true] "or 1101". Two questions. First: the example sentence on that row is P ∨ (¬Q ∧ R), which never mentions S. Is 1101 still a possible world for it? Second: what plays the role of "1101" in the first-order logic row?
Yes. A possible world assigns a truth value to every symbol in the language, not only to the symbols that appear in the sentence you happen to be looking at. If the language is {P,Q,R,S} then a world is four bits, and a sentence mentioning three of them simply does not care about the fourth. This is why the number of worlds is 2 to the power n in the number of symbols, and why the truth tables in section 4 always have 2^n rows even when a column is constant.
In first-order logic there is no bit string. A possible world is: a set of objects (o1, o2, o3 on the slide), a set of tuples for each predicate (P holds for <o1,o2>, Q holds for <o3>), a value for each function (f(o1)=o1), and an object for each constant (Joe=o3). Deck p.31 spells out this same list in full.
This slide says relational databases "Cannot express disjunction, implication, universals, etc." and that their semantics are "sentences in the DB are true, everything else is false". Name the assumption in that second phrase, and explain in one line why it is what makes the first phrase true.
The closed-world assumption: anything not recorded is taken to be false. A database therefore has exactly one model, so there is nothing for a disjunction to be uncertain between. Disjunction and implication earn their keep only when several worlds are still open, which is precisely the situation propositional logic and a SAT solver are built for.
Worth carrying forward: Part 11 uses the closed-world assumption for the initial state of a planning problem, and does not use it for the goal state. That asymmetry is a Part 11 exam point.
The slide's other example, knowledge graphs, is "roughly: relational DB + ontology of types and relations", with the Google Knowledge Graph quoted at 5 billion entities, 500 billion facts and more than 30 percent of queries, and the Facebook network at 2.8 billion people. It is background, not machinery.
Deck p.13 defines the relation everything else serves:
and immediately restates it as a statement about sets: "the α-worlds are a subset of the β-worlds [models(α) ⊆ models(β)]". The word model is used here in its logician's sense, a possible world in which the sentence is true. It is not the sense of "the model" in a Markov decision process, where the model is the transition function.
The slide says α2 is ¬Q ∧ R ∧ S ∧ W and α1 is ¬Q. One of the two circles on the picture contains exactly one world; the other contains many. Which is which, and which sentence entails the other? State the general rule in one line.
α2 is the small green circle (one world on the picture): it pins down four symbols at once, so few worlds satisfy it. α1 is the large red region: it constrains only Q, so many worlds satisfy it. The slide's conclusion is α2 ⊨ α1.
The rule: the stronger sentence has the smaller model set, and the stronger sentence entails the weaker one. Adding a conjunct shrinks the model set and can only make a sentence entail more. This is worth over-learning because the arrow points the opposite way to the intuition of "bigger means more": the sentence with more content has fewer models.
Deck p.14 then defines what a proof is and the two properties an inference algorithm can have:
Deck p.15 gives the two families of method, and it is worth naming them now because the rest of the Part is one of each:
Constructed, in the 2023 sample theory paper's true/false format
An inference algorithm that is sound but not complete may fail to prove something that is entailed, but everything it does prove is entailed.
Deck p.17 gives the syntax as a closed list of formation rules. Given a set of proposition symbols {X1, X2, ..., Xn}, with True and False often added for convenience:
The last line of the slide is the one students skip: "And p.s. there are no other sentences!" That closure clause is what makes the four-step CNF recipe of section 8 complete. There are only five connectives to eliminate, so a recipe that handles all five handles everything.
Compare this list with the first-order syntax you will meet on deck p.36. Name the two syntactic devices first-order logic adds. Then say what a propositional symbol can and cannot stand for.
First-order logic adds (i) terms with structure: constants, logical variables and functions applied to terms, so that predicates can take arguments; and (ii) quantifiers, ∀ and ∃. The five connectives carry over unchanged.
A propositional symbol stands for one whole fact that is true or false, such as "it is raining". It cannot be decomposed: it has no arguments, so "Raining in Bruges" and "Raining in Ghent" are two unrelated symbols with no shared structure. That is why the rules of chess cost 100,000 pages here and one page in first-order logic (deck p.30).
Deck p.18 gives the semantics. Let m be a model assigning true or false to the symbols. Then:
| Sentence | Is true in m iff |
|---|---|
| Xi | its truth value is given in m |
| ¬α | α is false in m |
| α ∧ β | α is true in m and β is true in m |
| α ∨ β | α is true in m or β is true in m |
| α ⇒ β | α is false in m or β is true in m |
| α ⇔ β | α ⇒ β is true in m and β ⇒ α is true in m |
Write out the four rows of the truth table for α ⇒ β using only the rule on this slide. Then answer: if α is false, what can you say about the truth of α ⇒ β, whatever β is?
Reading "α is false in m or β is true in m" straight off the slide: F,F → T; F,T → T; T,F → F; T,T → T. An implication is false in exactly one case, antecedent true and consequent false.
If α is false the implication is true regardless of β. This is called vacuous truth, and it is the mechanism behind two things later in this chapter: the first-order sentence ∀x (movable(x) ⇒ blue(x)) is true in a world with no movable objects, and the whole conditional in the exercise session 5 multiple choice is true whenever its antecedent fails.
an implication just doesn't exist. What exists is this thing [not-A or B]... if you're ever confused about the intuition behind implication... just reduce it to what it actually genuinely represents.(Lecturer, T10 exercise session). This is the single most useful sentence in the whole exercise session. Every time an implication confuses you, rewrite it as ¬α ∨ β and the confusion goes away. It is also step 2 of the CNF recipe, so you are practising the recipe every time you do it.
Exercise session 7, section 2.1, verbatim
SAT from beginning to end. Consider the theory consisting of the following natural language statements: 1. I will get fit if and only if I run. 2. If I run and I do not rest, I will get injured. 3. I run if and only if I'm not injured. 2.1 Translate to propositional logic. Translate these statements into propositional logic.
Four symbols: Fit, Run, Rest, Injured. Then
and the slide adds the line that matters for parts 2.2 to 2.4: "The theory is the conjunction of 1, 2 and 3".
What earns the marks: choosing one symbol per atomic fact and no more (four symbols, not five: "I do not rest" is ¬Rest, not a new symbol NotRest); getting the direction of statement 2 right, with the conjunction in the antecedent; and noticing that "if and only if" is ⇔ while "if" alone is a one-way ⇒. Statement 2 has no biconditional even though it sounds symmetrical in English.
Model checking is the brute-force method, and for propositional logic it is always available because the number of worlds is finite: 2n for n symbols. To test whether two sentences mean the same thing, you build one row per world and check that the two sentences agree in every row. To test entailment α ⊨ β, you check every row in which α is true and confirm β is true there too.
The exercise session's own advice, which is also the marking advice, is to give each subexpression its own column. You are much less likely to make an arithmetic slip on a five-symbol sentence if the two operands are already sitting in columns beside it.
Exercise session 7, section 1 (Model checking), verbatim
Determine whether A ⇒ (B ⇒ C) is semantically equivalent to (A ∧ B) ⇒ C by checking whether these two sentences have the same truth value in every world.
Three symbols, so 23 = 8 worlds. Semantic equivalence means the last two columns are identical in every one of them.
| A | B | C | A ∧ B | B ⇒ C | A ⇒ (B ⇒ C) | (A ∧ B) ⇒ C |
|---|---|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 1 | 1 | 1 |
| 0 | 0 | 1 | 0 | 1 | 1 | 1 |
| 0 | 1 | 0 | 0 | 0 | 1 | 1 |
| 0 | 1 | 1 | 0 | 1 | 1 | 1 |
| 1 | 0 | 0 | 0 | 1 | 1 | 1 |
| 1 | 0 | 1 | 0 | 1 | 1 | 1 |
| 1 | 1 | 0 | 1 | 0 | 0 | 0 |
| 1 | 1 | 1 | 1 | 1 | 1 | 1 |
Row 3 (A=0, B=1, C=0) is the row worth checking by hand: B ⇒ C is false there, yet A ⇒ (B ⇒ C) is true, because A is false and a false antecedent makes the whole implication true. Students who get this row wrong have applied ⇒ as if it were ∧.
What earns the marks: writing the words "in every world" or equivalent, and showing all 8 rows. A truth table with 6 rows is an incomplete proof of equivalence, and a table that stops as soon as the two columns first agree proves nothing at all.
Question style: "Determine whether X is semantically equivalent to Y by checking whether these two sentences have the same truth value in every world" (exercise session 7, section 1). The same machinery, with the target sentence negated, is what section 2.2 of the same session uses to verify entailment.
Classic mistake: checking only some worlds and concluding equivalence. Equivalence and entailment are both universally quantified over worlds, so a partial table can refute them but can never establish them. The second classic mistake is the implication row: an implication with a false antecedent is true, and a table that marks it false will still look internally consistent, so the error survives checking.
Cost control: the table doubles with every extra symbol. Four symbols is 16 rows, which is what section 2.2 needs and what the exercise-session slide actually shows. Beyond a handful of symbols the table stops being writable by hand, which is the pedagogical point of meeting the slow method first: sections 7 to 9 exist because this one does not scale.
Deck p.19 defines satisfiable: a sentence is satisfiable if it is true in at least one world. Then it asks the question that turns a solver into a reasoner. Suppose you have a hyper-efficient SAT solver. How do you use it to test entailment? The slide gives a four-line chain:
Line 3 to line 4 is the only step with content, and it is the implication rule of deck p.18 read backwards: ¬(α ⇒ β) is ¬(¬α ∨ β), which De Morgan turns into α ∧ ¬β. The slide's summary of the recipe: "add the negated conclusion to what you know, test for (un)satisfiability; also known as reductio ad absurdum". Its last line is the reason section 8 exists: "Efficient SAT solvers operate on conjunctive normal form".
You hand the solver α ∧ ¬β. It comes back with a satisfying model. What have you learned? And what have you learned if it comes back "unsatisfiable"? State both in terms of α ⊨ β.
Satisfiable means the solver found a world in which everything you know is true and the conclusion is false. That world is a counterexample: α does not entail β, and the returned model is the proof, which is worth writing down in an exam because it is checkable.
Unsatisfiable means no such world exists, so in every world where α holds, β holds: α ⊨ β.
The direction is inverted relative to intuition, which is why students report the wrong conclusion under time pressure. A useful phrase to write down first: "I want the solver to fail."
this is still [NP]-complete... you can still construct problems for which it can take an exponential amount of time.(Lecturer, T9), said about the hyper-efficient SAT solver of deck p.19, which prints the warning "WARNING: NP-COMPLETE" in capitals on the slide itself. Two things follow. First, "efficient in practice" and "polynomial" are different claims, and the deck only makes the first. Second, the same sentence closes the summary on p.43: SAT is "the mother of all formal languages, with highly efficient SAT solvers (still NP though)".
as a side note they will only accept sentences in conjunctive normal form.(Lecturer, T9), said at the point where the reduction is finished and the input format becomes the obstacle. This is the hinge between section 7 and section 8: the reduction gives you α ∧ ¬β, but that sentence is in whatever shape the English happened to produce, and a solver will not read it until you have converted it.
Exercise session 7, section 2.2 (Verify entailment), verbatim
Determine whether this theory entails the statement: 'I will rest if I get fit.'
Step 1, translate the query. "I will rest if I get fit" is Fit ⇒ Rest, not Rest ⇒ Fit. In English, "X if Y" puts Y in the antecedent. This is where most of the marks are lost.
Step 2, negate it and simplify (the session does this explicitly on its slide):
Step 3, test the conjunction of four sentences for satisfiability: 1) Fit ⇔ Run, 2) Run ∧ ¬Rest ⇒ Injured, 3) Run ⇔ ¬Injured, 4) Fit ∧ ¬Rest. The slide's own phrasing: "If the conjunction of these 4 sentences does not hold in all worlds, then our original statement is entailed!"
Step 4, the 16-row table. Four symbols, 16 worlds. The theory (sentences 1, 2 and 3 together) is true in exactly three worlds:
| Fit | Run | Rest | Injured | status |
|---|---|---|---|---|
| 0 | 0 | 0 | 1 | model of the theory; sentence 4 is false here |
| 0 | 0 | 1 | 1 | model of the theory; sentence 4 is false here |
| 1 | 1 | 1 | 0 | model of the theory; sentence 4 is false here |
Conclusion. The conjunction of all four is false in all 16 worlds, so it is unsatisfiable, so the theory entails Fit ⇒ Rest. The session's slide says it in three words: "Thus, it is confirmed!"
Sanity check you can do in the exam without the full table: in every model of the theory, either Rest is true (rows 2 and 3) or Fit is false (rows 1 and 2), and Fit ⇒ Rest needs exactly one of those. Row 1 is the interesting one: Fit is false, so the implication is vacuously true.
Deck p.21 gives three definitions that nest inside each other. Read them from the inside out:
So CNF is a two-level sandwich with a fixed order: and on the outside, or on the inside, negations only on symbols. Nothing else is allowed, and in particular no ⇒ and no ⇔. The deck's first line, "Every sentence can be expressed as a conjunction of clauses", is what makes the restriction harmless: you never lose expressive power by converting, you only pay in length.
The exercise sheet numbers the four steps; deck p.21 shows the same four applied to one example, with "push down ¬" in a side box. Apply them in this order and no other:
Reference item 51 records the order as it was said aloud in the session, and it is the same order as deck p.21: equivalence first, then implication, then push negations inward, then distribute or over and. The session also states the reason step 4 goes that way and not the other: distributing ∧ over ∨ is legal too, but it produces disjunctive normal form, which is not what a SAT solver reads.
(Exercise session 7, T10; paraphrase of the spoken order as recorded in the shared reference, not a verbatim quotation.)Why the order matters: step 3 cannot finish while implications are still present, because ⇒ hides a negation you have not written down yet, and step 4 cannot start until every negation is already sitting on a symbol, because distribution assumes its operands are pure disjunctions and conjunctions. Running the steps out of order is the most common way to produce something that looks like CNF but is not equivalent to the original.
The worked example starts from At_11_0 ⇒ (Wall_01 ⇔ Blocked_W_0) and ends with two clauses. Line 3 of the slide is ¬At_11_0 ∨ ((¬Wall_01 ∨ Blocked_W_0) ∧ (¬Blocked_W_0 ∨ Wall_01)). Name the step that produced it, say why the sentence is still not in CNF at that point, and name what step 4 does to it.
Line 3 comes from step 2, eliminate ⇒, applied three times at once: to the outer implication and to both of the inner ones that step 1 created.
It is not CNF because the top-level connective is ∨ with a conjunction inside its right operand. CNF requires ∧ on the outside. The offending shape is exactly α ∨ (β ∧ γ).
Step 4 distributes that ∨ over the ∧, copying ¬At_11_0 into both halves:
Two clauses of three literals each. All four lines of the slide were checked in Python over all 8 worlds and are equivalent, so the chain is sound as printed. Note the cost: one distribution turned one sentence into two clauses, and the shared literal ¬At_11_0 now appears twice. That duplication is why CNF conversion can blow up in length, which is the concrete version of the encoding-efficiency warning on deck p.5.
Exercise session 7, section 2.3 (Translate to conjunctive normal form), verbatim
Extend the original 3 statements with the claim 'If I run, I get tired and hungry' and translate them into the conjunctive normal form (CNF).
Take the four statements one at a time. Each row below is the session's own chain.
1) I will get fit if and only if I run.
2) If I run and I do not rest, I will get injured.
3) I run if and only if I'm not injured.
4) If I run, I get tired and hungry.
The seven clauses: (¬Fit ∨ Run), (¬Run ∨ Fit), (¬Run ∨ Rest ∨ Injured), (¬Run ∨ ¬Injured), (Injured ∨ Run), (¬Run ∨ Tired), (¬Run ∨ Hungry).
What earns the marks: writing the intermediate line for each step rather than jumping to the answer, because the steps are what is being assessed. Note that only statement 4 needs step 4 and only statements 2 and 3 need step 3, so a conversion in which every sentence uses every step is a sign that something has gone wrong.
Two traps visible here. In statement 2, ⇒ binds more weakly than ∧, so the antecedent is the whole of Run ∧ ¬Rest, and negating it gives ¬Run ∨ Rest by De Morgan, not ¬Run ∧ Rest. In statement 3, the second implication produces a double negation that step 3 must remove; leaving ¬¬Injured in place is not CNF, because a literal is a symbol or a negated symbol and nothing else.
Deck p.23 introduces DPLL (Davis-Putnam-Logemann-Loveland) as "the core of modern solvers" and describes it as a "Recursive depth-first search over models with some extras". The search skeleton is Part 4: pick an unassigned symbol, try true, recurse, and on failure try false. The extras are what make it fast, and they are what the exam asks you to apply.
The pseudocode calls FIND-PURE-SYMBOL and then FIND-UNIT-CLAUSE, and only reaches the branching line if both come back empty. Suppose at some node there is both a pure symbol and a unit clause. Which one does this pseudocode apply? And what is the one situation in which the printed order costs you something?
As printed, the pure symbol is applied first: FIND-PURE-SYMBOL is called before FIND-UNIT-CLAUSE, and each successful call returns immediately with a recursive call on a smaller symbol set. Both branches of the final line are only reached when neither rule applies, which is what "no unit clauses left, now we must guess" means.
The situation where the order costs you something is precisely the exam question in this session. The pure-literal rule preserves satisfiability, not the set of models: a pure positive symbol can safely be set true, but the models in which it is false are then never visited. If the question says "find all satisfying models", applying pure-literal elimination silently loses some of them. Exercise session 7 asks for "the DPLL algorithm with unit propagation" for exactly this reason, and the published search tree branches instead of using purity. Worked through in the exam question below.
Exercise session 7, section 2.4 (Apply the DPLL algorithm), verbatim
Use the DPLL algorithm with unit propagation to find all satisfying models of the theory consisting of the original 3 statements. Select the variables in alphabetical order.
Input. The CNF of statements 1 to 3 only, so the Tired and Hungry clauses from section 2.3 are dropped. Five clauses, four symbols:
Branching order. Alphabetical over {Fit, Injured, Rest, Run}, so the first guess is on Fit. After that, unit propagation decides every remaining symbol, so no further guess is needed on either branch.
root: (¬Fit,Run) (¬Run,Fit) (¬Run,Rest,Injured) (¬Run,¬Injured) (Injured,Run)
|
+-- Fit = 1 remaining: (Run) (¬Run,Rest,Injured) (¬Run,¬Injured) (Injured,Run)
| unit Run = 1 remaining: (Rest,Injured) (¬Injured)
| unit Injured = 0 remaining: (Rest)
| unit Rest = 1 remaining: none, all clauses satisfied
| MODEL 1: Fit, Run, ¬Injured, Rest
|
+-- Fit = 0 remaining: (¬Run) (¬Run,Rest,Injured) (¬Run,¬Injured) (Injured,Run)
unit Run = 0 remaining: (Injured)
unit Injured = 1 remaining: none, all clauses satisfied, Rest never assigned
MODEL 2: ¬Fit, ¬Run, Injured, Rest
MODEL 3: ¬Fit, ¬Run, Injured, ¬Rest
Three models, which is exactly the set of worlds found by the 16-row truth table in section 7. The two methods must agree, and checking that they do is the cheapest error check available to you in the exam.
The right branch is where the marks are. After Injured=1 every clause is satisfied and Rest is still unassigned. Early termination fires here (deck p.23: stop if all clauses are satisfied), and a free symbol means the leaf stands for two models, not one. The published solution writes both lines in the box for this reason. Reporting one model there, or continuing to branch on Rest and reporting four leaves, are the two ways to lose the point.
Why purity was not used. Rest occurs in only one clause, (¬Run ∨ Rest ∨ Injured), and only positively, so it is a pure positive literal at the root. The pseudocode on deck p.24 would set Rest=true immediately, return a satisfying model, and never produce MODEL 3. Confirmed in Python: Rest is the only symbol with a single sign in this clause set, and MODEL 3 is the only model with Rest false. When a question says find all models, propagate units and branch, and leave purity alone.
Drill this trace until it is mechanical, then run variants in the companion visualiser: viz-sat.html.
Question style: one story in English, then four sub-questions in order: translate to propositional logic, verify an entailment, convert to CNF, run DPLL. Exercise session 7 section 2 is the template, and it is the single longest exercise in the session.
Classic mistakes, one per stage: (1) inventing a symbol for a negated fact, or mis-reading "X if Y"; (2) forgetting to negate the conclusion before testing satisfiability, which tests the wrong sentence entirely; (3) distributing ∧ over ∨ instead of ∨ over ∧, which yields disjunctive normal form; (4) stopping at the first model when the question says all models, or forgetting that an unassigned symbol at a satisfied leaf doubles the model count.
Bookkeeping that earns marks: write the surviving clause set beside every node of the DPLL tree, in the published solution's own style, with the unit clause marked. A tree of bare assignments with no clause sets is not a trace of DPLL, it is a guess that happens to be right.
Model checking enumerates worlds. Theorem proving never mentions a world: it starts from the sentences you were given and grows the set by applying inference rules until the goal appears. Deck p.15 defines it as a search "for a sequence of proof steps (applications of inference rules) leading from α to β" and gives Modus Ponens as the example rule. The 2025-26 exercise session works forwards from the premises using three named rules.
| Rule | From | Infer | Read it as |
|---|---|---|---|
| Modus ponens | α, α ⇒ β | β | the antecedent holds, so the consequent does |
| Modus tollens | α ⇒ β, ¬β | ¬α | the consequent failed, so the antecedent must have failed |
| Addition | α | α ∨ β | a true disjunct makes any disjunction true, so you may add anything you like |
| Split conjunction | α ∧ β | α (and β) | a conjunction gives you each of its parts separately |
Addition looks useless when you first meet it, because it throws information away. Its job in a proof is shape-fitting: it converts a fact into the form some other rule needs. In the proof below it turns ¬C into ¬C ∨ ¬I, which is De Morgan's version of ¬(C ∧ I), which is exactly the negated consequent modus tollens needs for line 1.
Exercise session 7, section 4 (Theorem proving), verbatim
Use theorem proving to show that the following theory implies 'it rained'.
Step 1, choose symbols. The session's own choice, printed on its slide: It rains (R), It is foggy (F), The competition takes place (C), The road is inaccessible (I), A winner is determined (W).
Step 2, translate.
Step 3, the proof. Goal: derive 'it rained', that is R.
Line by line. (4): line 2 says C ⇒ W and line 3 says ¬W, so the consequent failed and modus tollens gives ¬C. (5): addition attaches ¬I, which costs nothing and produces ¬C ∨ ¬I, that is ¬(C ∧ I). (6): line 1 has consequent (C ∧ I) and line 5 is its negation, so modus tollens gives ¬(¬R ∨ ¬F), which pushed inwards is R ∧ F. (7): split the conjunction and take R.
Checked semantically: over all 32 worlds of {R,F,C,I,W} there is no world in which lines 1, 2 and 3 hold and R is false, and each of lines 4 to 7 holds in every model of the theory, so every step is sound as well as the conclusion.
What earns the marks: naming each rule and citing the line numbers it used, in the form the solution uses ("Modus tollens (2&3)"). A correct chain of formulas with no rule names is an incomplete answer to this question, because the question is about the rules. Note also that the proof establishes R ∧ F on the way, so it has shown that it both rained and was foggy; the question only asked for R, and line 7 is what makes the answer to the question explicit.
Question style: "Use theorem proving to show that the following theory implies X" (exercise session 7, section 4). Three or four English sentences, a vocabulary you choose yourself, and a target literal.
Classic mistake: writing a chain of true formulas without naming a rule for each line. The second is trying to run the proof backwards from the goal, which the session's format does not use: this is forward proof, and the entry point is always the fact with no antecedent, here ¬W.
Where to look for the first step: the shortest premise. ¬W is a bare literal, so it is the only thing that can trigger anything on its own, and it pairs with the only implication whose consequent is W.
Deck p.25 gives the size gap in one line: a naive implementation of DPLL solves about 100 variables; a real one solves about 100,000,000. The listed reasons are worth reading once and not memorising:
Every item on this slide is an engineering improvement. Name the property of the problem that none of them changes, and give the one-line consequence for what you may claim in an exam answer.
Satisfiability is NP-complete, and no amount of indexing changes that. Deck p.19 prints the warning and deck p.43 repeats it in the summary as "still NP though".
Consequence: you may write that modern solvers are "usually very efficient in practice" (deck p.27 uses those words) but not that DPLL runs in polynomial time or that the tricks make SAT tractable. The honest formulation is that the tricks shrink the constant and prune the tree, and there remain families of instances on which the search is exponential.
Deck p.26 lists where SAT solvers are actually used: circuit verification, software verification, software synthesis, protocol verification, protocol synthesis, and "Lots of combinatorial problems". Its last bullet closes the loop with Part 6: "Can even encode CSPs (over integers) into CNF and use SAT solver...". Deck p.27 is the propositional summary slide: inference algorithms determine whether α ⊨ β, theorem provers apply inference rules to construct proofs, model checkers such as SAT solvers enumerate models to establish entailment directly, and DPLL finds a possible model or proves there are none via recursive depth-first search.
Deck p.30 states the case for the upgrade in two lines. The rules of chess take 100,000 pages in propositional logic and one page in first-order logic (FOL). The rules of Pacman fit in one sentence:
The gain comes from structure. A propositional symbol is an unanalysed fact; a first-order atomic sentence has a predicate and arguments, so one sentence with a variable in it says what would need thousands of propositional symbols to say.
Deck p.31 lists the four ingredients. A possible world for FOL consists of: a non-empty set of objects; for each k-ary predicate, a set of k-tuples of objects (the tuples that satisfy it in this world); for each k-ary function, a mapping from k-tuples of objects to objects; and for each constant symbol, a particular object, with the note that constants can be thought of as 0-ary functions.
Deck pp.31 to 33 evaluate one sentence, Knows(A, BFF(B)), in three different worlds. BFF is a one-argument function ("best friend of"), Knows is a two-place predicate drawn as blue arrows, BFF is drawn as green arrows, and the grey arrows show which object each constant denotes.
Two objects. Knows holds between 1 and 2 in both directions. BFF(1)=2 and BFF(2)=1. A denotes 1 and B denotes 2. Work out the truth value of Knows(A, BFF(B)), showing the substitution at each step.
False, because there is no blue arrow from object 1 to itself: the pair <1,1> is not in the Knows relation of this world. The order of evaluation is the point: resolve constants to objects, then apply functions to get objects, then look the resulting tuple up in the predicate.
Compare this frame with the previous one. The objects, the Knows arrows and the BFF arrows are unchanged. Name the single thing that changed, and give the new truth value of Knows(A, BFF(B)).
Only the interpretation of the constant B changed: both grey arrows now point at object 1, so B denotes 1 instead of 2.
True. The lesson is that a sentence's truth value is a function of the world, and the constant-to-object mapping is part of the world just as much as the predicate tuples are. Nothing about the sentence changed at all.
Now there are three objects. Knows holds between 1 and 2 and between 2 and 3, in both directions, and nowhere else. BFF is the cycle 1 to 2 to 3 to 1. A denotes 1 and B denotes 2. Evaluate Knows(A, BFF(B)) again, and say which single arrow you would have to add to flip the answer.
False: there is no blue arrow between 1 and 3. This is the world used on deck p.35, which prints exactly this chain. Adding a single Knows arrow from 1 to 3 would make it true. Note that adding an arrow from 3 to 1 would not, because Knows takes an ordered pair and the sentence asks about <1,3>.
Deck p.34 defines a term, which is the part of the syntax that refers to an object. A term is one of three things: a constant symbol (A, B, EvilKingJohn), a function symbol applied to terms (BFF(EvilKingJohn)), or a logical variable (x). The slide's evaluation, in the three-object world, is BFF(EvilKingJohn) → BFF(2) → 3.
On this slide B denotes object 2, and EvilKingJohn also denotes object 2. Is that legal? What follows for the sentence B = EvilKingJohn, and what would break if you assumed otherwise?
Legal, and deliberate. Nothing in the definition of a possible world says distinct constants must denote distinct objects. Two names for one object is exactly the situation the equality predicate exists to describe, so in this world B = EvilKingJohn is true.
What breaks if you assume otherwise: you would conclude from Knows(A,B) and ¬Knows(A,EvilKingJohn) that the world is inconsistent, when in fact those two sentences simply cannot both hold once B and EvilKingJohn denote the same object. Assuming that distinct names denote distinct objects is a separate assumption, and the definition of a possible world on deck p.31 does not contain it: it asks for "a particular object" per constant symbol, not for a different one per constant symbol.
Deck p.35 defines an atomic sentence, the FOL counterpart of a propositional symbol. It is either a predicate symbol applied to terms, true iff the objects referred to by the terms stand in the relation referred to by the predicate, or an equality between terms, true iff the terms refer to the same object.
In the three-object world (BFF is the cycle 1 to 2 to 3 to 1, B denotes 2), evaluate BFF(BFF(BFF(B))) = B one application at a time.
True, exactly as printed on the slide. Evaluate from the inside out, one function application per line. Nested function terms are also where propositionalization gets into trouble in section 14: there are infinitely many terms of this shape, and a propositional encoding has to bound the nesting depth.
Deck p.36 and p.37 give the two quantifiers the same treatment: a quantified sentence is true in world w depending on the extensions of w, that is, on what happens when the variable is made to refer to each object of w in turn.
The sentence is ∀x Knows(x, BFF(x)) in the three-object world. Substitute x = 1, 2 and 3 in turn, evaluate each, and state the truth value of the whole sentence.
The whole sentence is false: ∀ needs every extension to be true, and the third fails because there is no Knows arrow between 3 and 1. Two out of three is not "mostly true"; there is no such thing.
The sentence is now ∃x Knows(x, BFF(x)), in the same world, with the same three substitutions. What is the truth value, and at which line may you stop?
True, and you may stop at the first line: x → 1 gives Knows(1,2), which is true, and ∃ needs only one witness. The slide still prints all three lines because it is reusing the previous slide, but the second and third add nothing.
The pairing worth remembering: ∀ is a big conjunction over the objects and fails at the first false case; ∃ is a big disjunction and succeeds at the first true case. That is also why the negation rules mirror De Morgan: ¬∀x φ is ∃x ¬φ, and ¬∃x φ is ∀x ¬φ.
This section is the one to over-prepare. It carries two of the exercise session's five exercises and the half of the 2023 sample exercise exam question 5 that the 2025-26 material still supports.
Almost every translation in this course is built from two templates, and mixing them up is the standard error:
Why they pair that way. With ∀, the implication is what lets objects that are not P off the hook: for a non-P object the antecedent is false and the implication is vacuously true, so the sentence says nothing about them, which is what "all P are Q" means. Writing ∀x (P(x) ∧ Q(x)) instead claims that everything in the world is a P and is a Q, which is far stronger and almost never what the English said. With ∃, the conjunction is what makes the witness do both jobs at once; writing ∃x (P(x) ⇒ Q(x)) is nearly vacuous, since any non-P object satisfies it.
Two of the three sentences on this slide differ only in which quantifier comes first: "There is someone that everyone knows" is ∃s Person(s) ∧ ∀n Person(n) ⇒ Knows(n,s), and "Everyone knows someone" is ∀x Person(x) ⇒ ∃y Person(y) ∧ Knows(x,y). Describe a world in which the second is true and the first is false, and say which of the two is the stronger sentence.
Take three people, Ann, Bo and Cy, where Ann knows Bo, Bo knows Cy and Cy knows Ann, and nothing else. Everyone knows someone, so the second sentence is true. But no single person is known by everyone: Bo is known only by Ann, Cy only by Bo, Ann only by Cy. So the first sentence is false.
∃∀ is the stronger sentence and entails the ∀∃ one, never the other way round. The ∃∀ form demands one witness that works for everybody; the ∀∃ form lets each person have a different witness. Deck p.40 uses precisely this pair as its entailment example: ∀x Knows(x,Obama) entails ∃y ∀x Knows(x,y), with the witness y = Obama.
Notice the first sentence's shape as well: ∃s Person(s) ∧ ... uses ∧ after ∃, and the inner ∀n Person(n) ⇒ ... uses ⇒ after ∀. Both templates appear in the same line.
The sentence is "Any two people of the same nationality speak a common language", written on the slide as ∀x,y (∃n Nationality(x,n) ∧ Nationality(y,n)) ⇒ (∃l Speaks(x,l) ∧ Speaks(y,l)). Explain what each of the two ∃ is doing, and say what would go wrong if the second one were moved outside the implication to the front of the sentence.
The first ∃n sits inside the antecedent and expresses "of the same nationality": there is some nationality n that x and y share. The second ∃l sits inside the consequent and expresses "a common language": there is some language l that both speak. Neither is a claim about all nationalities or all languages.
Moving ∃l to the front would give "there is one language l such that, for every pair of people of the same nationality, both speak l". That is the ∃∀ form again and it is much stronger: it demands a single universal language across all nationalities, whereas the original lets French speakers share French and Japanese speakers share Japanese. Same symbols, different scope, different claim.
Exercise session 7, section 3 (FOL knowledge representation), verbatim
A valid k-colouring of a graph has to satisfy the following statements:
Translate these sentences into first-order logic. You should use the predicates: coloured(x, y) (x has colour y), equal(x, y) (x equals y), edge(x, y) (x and y are connected by an edge). You should not use any functions.
Three things to notice, because they are the transferable technique.
1. "No ..." becomes ¬∃. Both negative constraints are written as "there does not exist a situation in which the bad thing happens". That is much easier to get right than the equivalent ∀ form, and it is equivalent: ¬∃v φ is the same sentence as ∀v ¬φ. If you prefer the ∀ form, the second statement becomes ∀v ∀c1 ∀c2 : ¬(coloured(v,c1) ∧ coloured(v,c2) ∧ c1 ≠ c2), and both forms are acceptable.
2. Inside an ∃, the connective is ∧. All three existential blocks list the conditions with ∧, exactly as the template says. An ⇒ inside one of them would break it.
3. The vocabulary constraint is doing real work. The sheet supplies equal(x,y) and forbids functions, so the slide's "c1 ≠ c2" is written with the supplied predicate as ¬equal(c1, c2). Without the ban on functions you would be tempted to write colour(v) = c, which quietly assumes every node has exactly one colour and makes the second statement unnecessary. Deciding whether something is a function or a relation is a modelling decision with consequences, which is why the sheet fixes it for you.
Also worth seeing: the first statement is the ∀∃ pattern from p.38, "every node has some colour", with a different colour permitted per node. That is the intended reading.
Exercise session 7, section 5 (FOL comprehension test), verbatim
Which of the following 4 first-order logic representations properly capture(s) the meaning of: 'If all movable objects are blue, then all non-movable objects are green.'
2023 sample exercise exam, question 5 (2.5 points), verbatim. Scope note attached.
Translate the following sentences to first-order logic. The available vocabulary consists of the predicates barber(x), man(x), shaves(x, y) (i.e. x shaves y).
(i) Not all men are barbers
(ii) There is a barber who shaves every man.
(iii) A barber shaves all men who do not shave themselves.
Now normalize the following first-order logic sentences into their clausal form.
(i) ∃x(barber(x) ∧ ¬∃y(shaves(y, x)))
(ii) ∀x(barber(x) ⇒ man(x) ∧ shaves(x, x))
The first half of this question, the three translations, is still live: exercise session 7 sections 3 and 5 practise exactly this skill in the 2025-26 material. The second half, normalization into clausal form, has no counterpart anywhere in the 2025-26 material, and neither does question 4's resolution refutation. Section 15 below sets out the evidence and the recommended reading. Treat the second half as likely retired, prepare the first half properly.
(i) Not all men are barbers.
Both are correct and equivalent; the second is the one that shows you know ¬∀ is ∃¬. The trap is writing ∀x (man(x) ⇒ ¬barber(x)), which says no man is a barber. "Not all" denies the universal, it does not universally deny.
(ii) There is a barber who shaves every man.
This is the ∃∀ shape from deck p.38: one barber must work for every man. Both templates appear: ∧ after the ∃, ⇒ after the ∀. Putting the ∀ outside would give "for every man there is some barber who shaves him", which is the weaker ∀∃ claim and a different sentence.
(iii) A barber shaves all men who do not shave themselves.
The relative clause "who do not shave themselves" restricts the men being quantified over, so it belongs in the antecedent alongside man(y), joined by ∧. The English article "a" is read existentially here, matching (ii). If you prefer the reading "every barber shaves all such men", write ∀x ( barber(x) ⇒ ∀y ( ... ) ) instead. State which reading you chose in one line: the sentence is genuinely ambiguous in English, and an examiner who wanted the other reading can still see that you understood the scope question, which is what the marks are for.
A historical aside you do not need but will enjoy: with the biconditional version of (iii), "shaves all and only the men who do not shave themselves", the theory becomes unsatisfiable if the barber is himself a man. That is Russell's barber paradox, and it is a good check that you have read the scope correctly.
Question style: either "Translate these sentences into first-order logic" with a supplied vocabulary and a ban on functions (exercise session 7 section 3; 2023 sample exercise question 5, first half), or "Which of the following representations properly capture(s) the meaning of ..." with four candidate formulas (exercise session 7 section 5).
Classic mistake: quantifier scope, in every one of its forms. Using ∧ after ∀ where ⇒ is needed. Using ⇒ after ∃ where ∧ is needed. Letting one quantifier cover both halves of a conditional when the English has two independent claims. Leaving a variable free outside the bracket that binds it. In the multiple-choice question all three distractors are one of these, which tells you what the session thinks is worth testing.
Discipline that pays: write the bracket structure before the symbols. Decide first how many quantifiers there are and what each one's scope is, then fill in the predicates. Then read your formula back into English, literally, and compare it with the original sentence: option 3's gloss "all things have to satisfy at least one of ..." is what that reading-back produces, and it obviously is not the English you started from.
Deck p.40 starts by saying that nothing changes: "Entailment is defined exactly as for propositional logic", in every world where α is true, β is also true. What changes is the answer you can get back. In propositional logic a query returns yes or no. In first-order logic, given an existentially quantified query, an inference engine can return a substitution (also called a binding) for the variables that makes the resulting sentence entailed:
The notation, from the same slide: ασ means applying substitution σ to sentence α. If α = ∀x Knows(x,y) and σ = {y/Obama} then ασ = ∀x Knows(x,Obama). This is the machinery that makes Prolog a programming language rather than a yes/no oracle: the bindings are the output.
Deck p.41 gives the first of two ways to answer such a query, and it is the one that reuses everything from the first half of this chapter. Propositionalization converts (KB ∧ ¬α) into propositional logic and hands it to a SAT solver, exactly as in section 7. The trick, in the slide's words, is to "replace variables with ground terms, convert atomic sentences to symbols":
Grounding ∀x Knows(x,Obama) over two constants gave two symbols. Now do the same for the slide's second example, ∀x Knows(Mother(x), x). Write the first two ground instances, then say why this case is different and what the slide does about it.
The difference is the function symbol. With constants only, the set of ground terms is finite and grounding terminates. With a function, Mother(Obama) is itself a term you can feed back into Mother, so there are infinitely many ground terms and the propositional encoding never finishes.
The fix on the slide is depth-bounded checking: "for k = 1 to infinity, use all possible terms of function nesting depth k". You ground to depth 1, ask the solver, then depth 2, and so on. This is iterative deepening from Part 4, with nesting depth in place of path length.
The slide's guarantee and its limit: "If entailed, will find a contradiction for some finite k (Herbrand); if not, may continue for ever; semidecidable." So the procedure is a decision procedure for yes and only a search for no. If the sentence is entailed you will eventually find out; if it is not, you may wait for ever without ever being told. Deck p.43 repeats this in the summary: "Inference is semidecidable in general; many problems are efficiently solvable in practice."
Deck p.42 gives the second way to answer a first-order query: do not ground anything, apply the inference rules directly to first-order sentences. The example is the oldest one in logic:
The general rule is Modus Ponens with a substitution bolted on, and the slide states it in one line: given α ⇒ β and α', where α' = ασ for some substitution σ, conclude βσ. The second example on the slide is the one worth working through, because the substitution touches both sentences.
The slide's second example gives Knows(x,Obama) and the rule Knows(y,z) ⇒ Likes(y,z). Write the substitution σ and the conclusion, then say what the surviving variable in the conclusion means.
σ = {y/x, z/Obama}, which turns the rule's antecedent Knows(y,z) into Knows(x,Obama), matching the fact. Applying the same σ to the consequent gives the conclusion Likes(x,Obama).
The surviving x is still universally quantified: the fact was "everyone knows Obama" with x free and implicitly universal, so the conclusion is "everyone likes Obama". Note that the substitution maps a variable to a variable (y to x), not only variables to constants. That is what makes the rule lifted: one rule application covers all the objects at once, instead of one application per object as grounding would need.
The slide ends with a list of systems that work this way: "Prolog (backward chaining), Datalog (forward chaining), production rule systems (forward chaining), resolution theorem provers".
I won't go into a lot of detail here just know that this um exists.(Lecturer, T9), said about lifted inference on deck p.42. This is an explicit scope limit: know what lifted inference is, know that it contrasts with propositionalization, know that Prolog is the example. You are not expected to execute a lifted inference procedure.
The 2023 sample exercise exam devotes 4 of its 10 points to two first-order questions, Q4 (1.5 points, resolution refutation with mgu) and Q5 (2.5 points, translation plus clausal form). Here is what the 2025-26 material actually contains, and what follows.
The inference: resolution with mgu and normalization to clausal form have most likely been replaced, and the natural replacement is CNF conversion plus DPLL, which this year's session drills at length (sections 8 and 9 above). This is a judgment about a syllabus, not a statement of fact about the 2026 paper. The lecturer's own words about the sample exam are "I of course won't ask uh the exact same questions" (Lecturer, T9), and the exam information says the exercise questions will be similar to what was practised in the exercise sessions.
the slides and the material for the exercise sessions uh are the main source of reference. So that's the basis of what you need to know uh for the evaluation.(Lecturer, T1), also stated on the Part 1 slides. This is the rule that decides the scope question above: the 50 deck pages and exercise session 7 are the basis, and neither contains resolution or clausal form. It also decides the other direction, which matters more: everything that is in session 7, including the parts that were never recorded, is in scope.
The second half of exercise session 7 (the first-order representation exercise, the theorem-proving exercise and the first-order multiple choice) was never recorded. The recording of that session stops during the CNF conversion of the third statement. Sections 3, 4 and 5 of the session therefore exist only as the assignment sheet and the solution slides.
Practical consequence: for those three exercises there is no spoken explanation to fall back on, so the solution slides are the whole of the source, and this chapter reconstructs the reasoning around them. Do not read the absence of a recording as a signal that the material is out of scope. It is the opposite of that: three of the session's five exercises are in that half, and two of the four archetypes for this Part (A28 and A29) live there.
2023 sample exercise exam, question 4 (1.5 points), verbatim. Marked likely retired, see the scope note above.
Consider the following theory (note: directed edge(x, y) indicates a directed edge starting in x and pointing to y)
Apply resolution to find a refutation that proves that: There exists a directed edge that starts in a blue node and points to a red node. Clearly describe each resolution step by stating the clauses that were selected and the mgu (most general unifying substitution) that was applied.
Status. The method this question names, resolution refutation with a most general unifier, has no teaching source in the 2025-26 deck or exercise session. Prepare it only if you have spare time after everything else in this chapter is fluent. What is worth taking from the question is its shape, because that shape survives: a small theory, a disjunction that forces a case split, and a claim to prove.
The claim, written out. ∃x ∃y ( directed_edge(x,y) ∧ blue(x) ∧ red(y) ). Note the shape: existential, so ∧ inside, per section 13.
A complete proof using only 2025-26 material, by case analysis on clause 3. Clause 3 is a disjunction, so one of its two disjuncts holds.
Both cases yield the claim, so the theory entails it. The two witnesses are different, which is exactly why the disjunction cannot simply be dropped and why the question uses a refutation in the first place: there is no single edge that works in both cases, only a guarantee that some edge works in each.
If the 2026 paper replaces this question, the most likely replacement, given what session 7 drills, is the section 9 chain: translate, convert to CNF, run DPLL. Notice that the case analysis above is precisely what DPLL would do to clause 3: branch on the symbol, and find that both branches lead to a satisfying situation. The habit of thought transfers even if the notation does not.
Deck pp.44 to 49 are the applications block. They were not reached in the Part 10 lecture and are shown at the start of the next session (T10) as a recap before planning begins. There is no method to execute here. Read it once, for the sense of what a logical representation plus a solver buys in industry.
Deck p.22 belongs to the same family: it links to a live demonstration of a small SAT problem, the "frietkot" problem, where a group of friends must choose a combination of sauces that satisfies everyone's preferences. Each preference is a clause; the demonstration shows unit propagation eliminating choices one at a time before any guessing is needed, which is section 9 in miniature.
| Term | Precise definition | Plain paraphrase | Exam phrasing |
|---|---|---|---|
| Knowledge base | A set of sentences in a formal language (p.7). Used declaratively: Tell it what it needs to know, then Ask it what to do, and the answers should follow from the knowledge base. | Everything the agent has been told, written down in one language. | "a knowledge base is ... a collection of sentences in a formal language" |
| Possible world / model | Propositional: an assignment of true or false to every symbol, so 2n of them for n symbols (p.9, p.18). First-order: a set of objects, a tuple set per predicate, a mapping per function, an object per constant (p.31). A model of a sentence is a world in which that sentence is true (p.13). | One complete way the world could be. A model is one of those in which your sentence comes out true. | "in CSP called: an assignment of values to the symbols" (p.18); "What is a world in the context of logic?" (exercise session 7) |
| Entailment (⊨) | α ⊨ β iff in every world where α is true, β is also true; equivalently models(α) ⊆ models(β) (p.13). | Whenever what you know holds, the conclusion holds too. | "Determine whether this theory entails the statement: 'I will rest if I get fit.'" (exercise session 7, section 2.2) |
| Satisfiable / unsatisfiable | A sentence is satisfiable if it is true in at least one world (p.19). Unsatisfiable means true in none. Testing satisfiability of α ∧ ¬β decides α ⊨ β: unsatisfiable means entailed. | Satisfiable: at least one way to make it true. Unsatisfiable: no way at all. | "add the negated conclusion to what you know, test for (un)satisfiability; also known as reductio ad absurdum" (p.19) |
| Sound and complete | Sound: everything the algorithm claims to prove is in fact entailed. Complete: everything that is entailed can be proved (p.14). Independent properties. | Sound: it never lies. Complete: it never misses anything. | "Sound algorithm: everything it claims to prove is in fact entailed" (p.14) |
| Model checking | Method 1 of inference: for every possible world in which α is true, check that β is true too (p.15). Finite and therefore always available in propositional logic; a SAT solver is a model checker (p.27). | Enumerate the worlds and look. | "by checking whether these two sentences have the same truth value in every world" (exercise session 7, section 1) |
| Theorem proving | Method 2 of inference: search for a sequence of proof steps, that is applications of inference rules, leading from α to β (p.15). This year's rules: modus ponens, modus tollens, addition, split conjunction. | Derive the conclusion from the premises, one named rule at a time. | "Use theorem proving to show that the following theory implies 'it rained'" (exercise session 7, section 4) |
| Literal | A symbol or a negated symbol (p.21). Nothing else: not a double negation, not a bracketed formula. | One fact, possibly with a "not" in front. | "a literal in propositional logic is a propositional symbol or its negation" (exercise sheet, session 7) |
| Clause | A disjunction of literals (p.21). A clause with one literal is a unit clause; the empty clause is false and signals failure. | A row of alternatives joined by "or". | "A clause is a disjunction of literals" (exercise sheet, session 7) |
| Conjunctive normal form (CNF) | A conjunction of clauses (p.21). Reached by four steps in order: eliminate ⇔, eliminate ⇒, push ¬ inwards, distribute ∨ over ∧. Every sentence has one. | And on the outside, or on the inside, nots only on symbols. | "translate them into the conjunctive normal form (CNF)" (exercise session 7, section 2.3); "Efficient SAT solvers operate on conjunctive normal form" (p.19) |
| Unit clause, unit propagation | A clause left with a single literal; that literal's symbol must be set to satisfy it (p.23). Doing so shortens other clauses and often creates new unit clauses, which is the propagation. | Only one option left, so take it, then see what that forces. | "Use the DPLL algorithm with unit propagation to find all satisfying models" (exercise session 7, section 2.4) |
| Pure literal | A symbol whose occurrences in the as-yet-unsatisfied clauses all have the same sign; give it that value (p.23). Preserves satisfiability but not the full set of models, so do not use it when all models are wanted. | A symbol that is never contradicted, so let it have its way. | "pure literals (a symbol that always appears as either a positive or negative literal)" (exercise sheet, session 7) |
| DPLL | Davis-Putnam-Logemann-Loveland: recursive depth-first search over models with early termination, pure literals and unit clauses (pp.23 to 24). Returns true or false; the search tree records the models. | Backtracking search over true and false, with two shortcuts that avoid guessing. | "Apply DPLL. Write down the search tree defined by the DPLL algorithm for: ..." (exercise session 7 solutions) |
| Quantifier scope | The part of a formula a quantifier governs, fixed by brackets. ∀ pairs with ⇒, ∃ pairs with ∧. A variable outside its quantifier's brackets is free, and a formula with a free variable is not a sentence. | Which piece of the formula the "for all" or "there exists" is talking about. | "Which of the following 4 first-order logic representations properly capture(s) the meaning of ..." (exercise session 7, section 5) |
| Propositionalization | Converting (KB ∧ ¬α) from first-order to propositional logic by replacing variables with ground terms and atomic sentences with symbols, then calling a SAT solver (p.41). With function symbols the term set is infinite, so it is run depth-bounded, and inference is semidecidable. | Grind the first-order sentences down into propositional ones and reuse the SAT solver. | "If entailed, will find a contradiction for some finite k (Herbrand); if not, may continue for ever; semidecidable" (p.41) |
Constructed, in the 2023 sample theory paper's fill-in format (compare its questions 2.1 and 2.2)
Efficient SAT solvers operate on __________ normal form, in which the sentence is a conjunction of __________, each of which is a disjunction of __________. A clause left with a single one of these is called a __________ clause, and setting its symbol to satisfy it is called __________.
conjunctive normal form; a conjunction of clauses; each a disjunction of literals; a unit clause; setting its symbol is unit propagation.
The 2023 fill-in questions are worth 1 point each and are graded on the exact terms, so this is pure vocabulary recall. Two traps to avoid under time pressure: a clause is a disjunction, not a conjunction, and the outer connective of CNF is ∧, not ∨. If you can only remember one anchor, remember that the C in CNF describes the outside of the sentence.
Reference item 13 for the format: fill-in questions "can also be short answers that you need to provide", and "the boxes also give an indication of the expected length given a regular written font size" (Lecturer, T9). A one-word box wants one word.
Every truth table, CNF conversion, DPLL trace, entailment claim and first-order counterexample in this chapter was executed in Python before it was written down. The two published solution artefacts reproduced here, the eight-row equivalence table of exercise session 7 section 1 and the DPLL search tree of section 2.4, match the executed results cell for cell and node for node.