Resolution-Based Inference in Logical Systems, Explained

UPI Study › Courses › Introduction to Artificial Intelligence › Free lessons › Lesson 6.6 Free with a free account

Resolution-Based Inference in Logical Systems

Introduction to Artificial Intelligence · Chapter 6: Logic, Reasoning, and Knowledge SystemsSection 6.6 · lesson 44 of 6916 min · free with a free account

← Algorithms for Propositional ReasoningNext lesson: Structuring Domain Knowledge for AI Systems →

Earn 3 college credits for Introduction to Artificial IntelligenceRecommended for credit by NCCRS · Computer Science 373 · self-paced · one payment, lifetime access
Enroll in Introduction to Artificial Intelligence · $250 →Download the syllabus (PDF)

In this lesson

How the resolution rule proves queries by finding contradictions.

  • Convert propositional sentences to conjunctive normal form
  • Apply the resolution rule and use refutation to prove a query
  • Skolemize existential quantifiers and find most general unifiers
  • Explain soundness, refutation completeness and common resolution strategies

Free study notes

Get this lesson's notes by email

The key points and 4 practice questions with answers, in your inbox. One email, free.

One email. Unsubscribe in one click.

Transcript

Everything said in the video, section by section (2,295 words). Read along, or search it.

Opening Question

Can One Rule Prove Everything

A truth table settles any question in propositional logic, but it doubles in size with every new symbol. People proving a theorem don't work that way. They combine two known facts to get a new one. If rain makes the grass wet, and it's raining, then the grass is wet. And they keep going until the conclusion appears, or a contradiction does. Resolution turns that habit into one precise rule a program can apply over and over. J. A. Robinson introduced it in nineteen sixty-five. It's the engine inside many automated theorem provers, and a restricted form of it drives Prolog. So can one rule really prove everything that follows?

Clause Form

Literals, Clauses and the Empty Clause

Resolution works on conjunctive normal form, the shape from the last lesson. A literal is a symbol or its negation. On the board, the hook sign means not. A clause joins literals with OR, and it's true if at least one literal is. A CNF sentence is a list of clauses that must all be true. And one special clause matters most: the empty clause, written as a pair of brackets. It has no literals, so it can never be true. Deriving it means a contradiction has been found.

Conversion

Five Steps to Conjunctive Normal Form

Every propositional sentence can be rewritten in CNF by a fixed recipe of five steps. First, remove if-and-only-if: A iff B becomes A implies B, and B implies A. Second, remove implies: A implies B becomes not A or B, because an implication is false only when the first part is true and the second false. Third, push NOT inward with De Morgan's laws, until NOT touches only symbols. And double negation cancels. Fourth, distribute OR over AND. Fifth, split each AND part into its own clause, drop duplicate literals, and discard any clause containing both P and not P. Try it on, A iff B or C: A is true exactly when B or C is. Removing iff gives two implications. Removing implies turns each into an OR. Pushing NOT inward turns, not B or C, into not B and not C. Distributing OR over AND gives three clauses: not A or B or C, A or not B, and A or not C. A truth table confirms they match the original in every case. Simple rules convert at once. Rain implies Wet becomes the single clause, not R or W, and the fact Rain is just R. One warning. Distributing can make some sentences grow exponentially. The Tseitin transformation avoids that by naming sub-sentences with new symbols. It preserves satisfiability, not strict equivalence, and that's all a refutation proof needs.

The Resolution Rule

Cancel a Literal Against Its Opposite

Now the rule itself. Take two clauses, one containing a literal L, and the other containing its opposite, not L. Their resolvent is a new clause made of all the other literals from both. L or X, and not L or Y, give X or Y. A or B, with not B or C, resolves on B to give A or C. P, with not P or Q, gives Q: from P, and P implies Q, conclude Q. Not A or B, with not B or C, gives not A or C, chaining two implications. And P with not P gives the empty clause: a direct contradiction. Resolve one pair at a time. A or B, with not A or not B, resolved on A, gives B or not B: a tautology that says nothing, so discard it.

Soundness

Why a Resolvent Never Claims More

Why is the rule safe? Suppose both parent clauses are true. If L is true, then not L is false, so the second clause needs Y to be true. If L is false, the first clause needs X to be true. Either way, X or Y is true. So a resolvent never claims more than its parents already did. That property is called soundness.

Quick Check

Resolving on B Keeps Everything Else

Quick check. Resolve these two clauses: not A or B, and, not B or not C or D. Is the resolvent, not A or not C or D? Is it, not A or D? Or is it, not A or B or not C or D? Pause, and decide. The first. B and not B cancel, and every other literal stays: not A, not C, and D. The second drops not C, which the rule never does. And the third keeps B, but the pair you resolve on is exactly what disappears.

Refutation

Negate the Query, Seek a Contradiction

To prove a query, resolution doesn't search for it directly. It assumes the opposite, and looks for a contradiction. Convert the knowledge base to clauses. Negate the query, convert it, and add it to the list. Then resolve pairs again and again, adding each new resolvent. If the empty clause appears, the knowledge base together with not Q is impossible, so Q is entailed. If no new clause can be made, and the empty clause never appeared, Q isn't entailed. That last verdict holds for propositional logic.

Worked Example

Proving the Path Is Slippery

Use the knowledge base from earlier lessons. Rain makes the grass wet, the sprinkler makes the grass wet, wet grass makes the path slippery, and it's raining. As clauses: not R or W, not S or W, not W or Sl, and R. The query is Slippery, so add its negation, not Sl. Resolve clauses one and four on R, to get W. Resolve three with that W, to get Sl. And Sl, with clause five, not Sl, gives the empty clause: a contradiction. So the path is slippery. Clause two was never needed. Eight clauses, and three resolution steps, settled a question that a truth table would answer with sixteen rows. With many symbols, that gap grows enormously.

Worked Example

When the Empty Clause Never Appears

Now ask about the Sprinkler, which the knowledge base doesn't settle. Add not S to clauses one to four. Resolution can make four new clauses: W, Sl, not S or Sl, and not R or Sl. After that, no pair produces anything new. The clause not S would have to meet a clause containing S, and none does. The empty clause never appears, so Sprinkler isn't entailed. In propositional logic, this check always ends. Each symbol can appear in a clause positively, negatively, or not at all, so with n symbols there are at most three to the n clauses.

Quick Check

The Alarm Did Not Sound

Quick check, with a new knowledge base. If the alarm sounds, the dog barks. If the dog barks, the neighbor wakes. And the neighbor did not wake. Query: the alarm did not sound. As clauses, the knowledge base is not A or B, not B or N, and not N. Which clause do you add, and what happens? Add A, and the empty clause appears? Add not A, and it appears? Or add A, and the clauses run out? Pause, and decide. Add A, and the empty clause appears. The query is not A, so its negation is A. A with not A or B gives B. B with not B or N gives N. And N with not N gives the empty clause. So the alarm did not sound. Adding not A would just repeat the query, and nothing could clash with it.

First-Order Logic

Six Steps for First-Order Conversion

First-order logic adds constants like Anna, variables like x and y, predicates like Student of x, functions like Mother of x, and the quantifiers for all and exists. Here, variables are lowercase, and everything else starts with a capital letter. Resolution still works, but two new problems appear: removing quantifiers, and matching literals that contain variables. Conversion takes six steps. Remove iff and implies. Push NOT inward, now also through quantifiers. Standardize variables apart, so no two quantifiers share a name. Skolemize, to remove each exists. Drop for all, since every remaining variable is universal. Then distribute and split, as before.

Skolemization

Skolem Constants and Skolem Functions

Exists says something is there, without naming it. Skolemization gives it a name. If the exists isn't inside any for all, the name is a Skolem constant. There exists a dragon becomes Dragon of C1, where C1 names some particular dragon. Inside a for all, the thing may depend on the variable, so the name is a Skolem function. Everyone loves someone becomes Loves x, F of x, where F of x is whoever x loves. Every student has a teacher becomes, not Student of x, or Teaches T of x, x. And using a constant for everyone loves someone is wrong: it says everyone loves the same person. A Skolemized sentence isn't equivalent to the original, since it adds names. But it's satisfiable exactly when the original is, and that's enough for refutation.

Unification

Most General Unifiers and the Occurs Check

Next, matching. Student of Anna and not Student of x don't look exactly opposite. Unification finds a substitution that makes two expressions identical, here x slash Anna. The most general unifier commits to as little as possible. Knows Anna x, and Knows y Bob, unify with y as Anna and x as Bob. Loves x, Mother of x, and Loves Anna y, unify with x as Anna and y as Mother of Anna. And a variable can match a Skolem term too. Some pairs fail. Knows Anna x, and Knows x Bob, would need x to be both Anna and Bob, though renaming one x fixes it. Knows x x can't match Knows Anna Bob. And Q of x can't match Q of F of x: x would have to equal something containing itself. Checking for that is called the occurs check. A program unifies with four rules. If the two expressions are identical, succeed. If one is a variable, bind it to the other, unless the variable occurs inside it. That's the occurs check, and then it fails. If both are compound, with the same name and number of arguments, unify the arguments left to right, applying each binding to the rest. Otherwise, fail.

Quick Check

A Function Term Cannot Match a Constant

Quick check. Try to unify, Sees x, F of x, with, Sees Ann, Ann. Is the unifier x slash Ann? Is it x slash Ann, with F of x slash Ann? Or does no unifier exist? Pause, and decide. Unification fails: no unifier exists. The first arguments give x slash Ann. Apply it, and the second arguments become F of Ann and Ann. F of Ann is a function term and Ann is a constant, so the names differ, and rule four fails. Only variables can be bound. F of x isn't a variable, so a substitution can't send it to Ann.

Worked Example

Someone Is Employed via a Skolem Term

First-order resolution resolves two clauses, when a literal in one unifies with the opposite of a literal in the other. Then it applies the unifier to everything left. And the two clauses get different variable names first. Knowledge: every student has a teacher, anyone who teaches is employed, and Anna is a student. Query: is someone employed? The negated query, nobody is employed, becomes not Employed of z. Resolve one and three, with x as Anna: Teaches T of Anna, Anna. Resolve that with two: Employed T of Anna. And with the negated query, z as T of Anna, the empty clause appears. The proof never needed to know who Anna's teacher is. The Skolem term T of Anna stood in for that unnamed person. So someone is employed.

Completeness

Sound and Refutation Complete

So, can one rule prove everything that follows? Resolution is sound: deriving the empty clause really does show a contradiction. And it's refutation complete, as Robinson proved in nineteen sixty-five, for both propositional and first-order logic. If a set of clauses can't all be true, some sequence of steps derives the empty clause. Completeness is for refutation. Resolution may never write an entailed sentence out as a clause, but any entailed sentence can be proved by adding its negation. Propositional runs always stop. First-order runs don't: if the query is entailed, a proof is eventually found. If not, the search may run forever, because first-order entailment is only semi-decidable.

Search Strategies

Unit Preference, Set of Support, Linear Resolution

Generating every resolvent wastes effort, since most have nothing to do with the query. Strategies restrict or order the steps. Delete tautologies, and clauses less general than ones you hold: P makes P or Q redundant. Unit preference favors single-literal clauses, because the resolvent comes out shorter. Set of support makes every step use the negated query or something derived from it. It stays complete if the rest of the knowledge base is consistent. Input resolution makes every step use an original clause. And linear resolution always uses the latest resolvent, searching backward from the goal. Prolog works that way. Both are complete for Horn clauses. A Horn clause has at most one positive literal. Not A or not B or C reads as a rule: if A and B, then C. Many practical knowledge bases are written this way.

Trade-Off

When Restrictions Break Completeness

Set of support pays off as a knowledge base grows: it never wanders into rules that have nothing to do with the query. But a restriction can break completeness. Take four clauses: P or Q, not P or Q, P or not Q, and not P or not Q. They can't all be true. Full resolution finds the empty clause. The first two give Q, the last two give not Q, and Q with not Q gives the empty clause. Under input resolution, that last step is blocked: Q and not Q are both derived, not original. No original clause is a single literal, so the empty clause can never appear. Modern provers combine many refinements like these. In nineteen ninety-six, one of them, called EQP, settled the Robbins conjecture, an algebra question that had stood open for decades.

Key Takeaways

Clauses, Refutation and Unification

To sum up. Resolution needs clauses, and a five-step recipe converts any sentence to CNF. The rule cancels a literal against its opposite and keeps everything else, and it's sound. To prove a query, add its negation and look for the empty clause. First-order resolution adds Skolemization and unification. And resolution is refutation complete, though a first-order search may never end.

About Introduction to Artificial Intelligence at UPI Study

Introduction to Artificial Intelligence (Computer Science 373) is a self-paced online course of 69 video lessons in 9 chapters, from intelligent agents and search to game strategy, neural networks, logic and reasoning, machine learning, language, robotics and AI ethics. It carries a NCCRS credit recommendation for 3 semester credits.

Every lesson transcript is free on pages like this one, and the videos are free with a free UPI Study account. Enrolling adds a practice quiz after each lesson, the graded work and final exam that earn the credit, lifetime access, and an official transcript on completion. UPI Study has helped over 130,000 students with college credits. ACE and NCCRS have over 2,100 cooperating colleges that will consider accepting credits; the final decision is with the universities.

Enroll now → Course details Download the syllabus All Computer Science courses Every course with PRO →

Compare: AI vs Current Trends in CS and IT

Why take it here

Why students take Introduction to Artificial Intelligence with UPI Study

How machines search, reason and learnIntroduction to Artificial Intelligence covers how AI systems are built: intelligent agents, search and heuristics, game strategy, logic, neural networks, machine learning, language and perception, and the ethics of AI. It is a common upper-level course in computer science degrees.
Credit at a fraction of the priceThe same 3 credits can cost $750 or more at a US college. Here it is one payment, self-paced, with lifetime access.
Finish your degree soonerTransfer credits reduce the courses you still owe, so you can graduate earlier or lighten a heavy semester.
Strengthen an applicationA completed college-level course on an official transcript shows admissions and scholarship committees you can do the work.
Study on your own scheduleNo start dates, no deadlines. Watch the lessons, practice, and take the final when you are ready.
130,000+students helped with college creditsACE and NCCRS have over 2,100 cooperating colleges that will consider accepting credits; the final decision is with the universities.

Where the credit goes

Universities that work with NCCRS

Introduction to Artificial Intelligence carries a NCCRS credit recommendation. These universities work with NCCRS; some are UPI Study's signed partners. ACE and NCCRS have over 2,100 cooperating colleges that will consider accepting credits; the final decision is with the universities.

Thomas Edison State UniversityThomas Edison State UniversitySigned partnerUniversity of the PeopleUniversity of the PeopleSigned partnerCharter Oak State CollegeCharter Oak State CollegeSigned partnerStrayer UniversityStrayer UniversitySigned partnerColumbia Southern UniversityColumbia Southern UniversitySigned partnerIndiana TechIndiana TechSigned partnerPenn StatePenn StateWorks with NCCRSSouthern New Hampshire UniversitySouthern New Hampshire UniversityWorks with NCCRSSUNYSUNYWorks with NCCRS +many more cooperating universitiesFind my college →

Find my college → Not listed? Ask Athena in the corner of this page, or book a 15-minute call.

FAQ

Questions students ask us

About Resolution-Based Inference in Logical Systems

What is the resolution rule in logic?
The resolution rule takes two clauses, one containing a literal L and the other its opposite NOT L, and produces a new clause from all their remaining literals. L OR X and NOT L OR Y give X OR Y. For example, P with NOT P OR Q gives Q, and P with NOT P gives the empty clause, a contradiction. J. A. Robinson introduced it in 1965.
How does proof by refutation work with resolution?
Proof by refutation adds the negation of the query to the knowledge base clauses, then resolves pairs until the empty clause appears. If it does, the knowledge base together with the negated query is impossible, so the query is entailed. With NOT Rain OR Wet, NOT Wet OR Slippery, Rain and the negated query NOT Slippery, three resolution steps reach the empty clause, proving Slippery.
What is Skolemization in first-order logic?
Skolemization removes existential quantifiers by naming the object they promise. Outside any universal quantifier, the name is a Skolem constant, so there exists a dragon becomes Dragon(C1). Inside one, it is a Skolem function of the variable, so everyone loves someone becomes Loves(x, F(x)). Using a constant there is a common mistake, since it says everyone loves the same person.
What is the occurs check in unification?
The occurs check stops a variable from being bound to a term that contains that same variable. Q(x) cannot unify with Q(F(x)), because x would have to equal something containing itself. Otherwise, unification finds the most general substitution that makes two expressions identical, such as y as Anna and x as Bob for Knows(Anna, x) and Knows(y, Bob).

About the Introduction to Artificial Intelligence course

How many college credits is Introduction to Artificial Intelligence?
Introduction to Artificial Intelligence (Computer Science 373) carries a NCCRS credit recommendation for 3 semester credits. ACE and NCCRS have over 2,100 cooperating colleges that will consider accepting credits; the final decision is with the universities.
How much does Introduction to Artificial Intelligence cost and what is included?
$250, paid once, with lifetime access: all 69 video lessons, a practice quiz after each, the graded work and final exam, and an official transcript when you finish. Students who want several courses choose UPI Study PRO instead.
Which universities accept UPI Study credits?
UPI Study has signed partner agreements with universities such as Thomas Edison State University, University of the People and Charter Oak State College, and works with universities such as Penn State, SNHU and SUNY. ACE and NCCRS have over 2,100 cooperating colleges that will consider accepting credits; the final decision is with the universities. Use "Find my college" on this page to check yours.
How long does Introduction to Artificial Intelligence take?
It is self-paced with no deadlines. The 69 lessons total about 16 hours of video; most students add reading and practice time and finish in a few weeks to a few months, on their own schedule.
How are the exams done?
Quizzes and assignments are online in the course. The final exam is taken online with proctoring; a person on the UPI Study team checks assignments, usually within two days.
How do my credits reach my college?
When the course shows 100% complete, request the official transcript from your dashboard. It is sent to the college you name, and you can send it to more than one. Check your college first with "Find my college" on this page, or ask Athena.

Ready for the full course? Earn 3 credits in Introduction to Artificial Intelligence.

69 video lessons, a quiz after each one, and the graded work that earns the credit. Recommended for credit by NCCRS.

Enroll in Introduction to Artificial Intelligence →Download the syllabusEvery course with PRO →
Introduction to Artificial Intelligence
3 credits · NCCRSEnroll →