Python · Course navigation

Resolution and proof by refutation

Prove a conclusion by adding its negation to the clauses and deriving the empty clause.

On this page

Before you start

Propositional logic and sets.

Prove a conclusion by adding its negation to the clauses and deriving the empty clause.
Predict the sample output and explain the state changes.
Complete the practice task and check the boundary cases.

The concept

Resolution is an inference rule that works on clauses, which are disjunctions of literals (a symbol or its negation) such as ¬P ∨ Q. Any propositional sentence can be converted to conjunctive normal form, a conjunction of clauses, by eliminating implications, moving negations inward, and distributing or over and. Given two clauses that contain a literal and its complement, resolution produces a new clause containing all the remaining literals of both.

Resolution is used for proof by refutation. To show that a knowledge base entails Q, add ¬Q to its clauses and apply resolution repeatedly. If the empty clause, a contradiction, is derived, then KB ∧ ¬Q is unsatisfiable and so KB entails Q. If no new clauses can be generated and the empty clause has not appeared, Q is not entailed. Resolution is sound, and it is refutation-complete: it will find a contradiction whenever one exists. It was made practical for automated theorem proving by J. A. Robinson's 1965 paper.

The knowledge base here encodes P ⇒ Q, Q ⇒ R, and the fact P. Negating the query R and resolving yields the empty clause, so R is entailed. For an unrelated symbol S, the saturation of all possible resolvents never produces the empty clause, so the program correctly reports that S is not entailed. In the code, a clause is a frozenset of literals, and ~ marks negation.

Code example

Python

from itertools import combinations


def negate(literal):
    return literal[1:] if literal.startswith("~") else "~" + literal


def resolve(first, second):
    return [(first - {lit}) | (second - {negate(lit)}) for lit in first if negate(lit) in second]


def refutes(clauses):
    clauses = set(clauses)
    while True:
        new = set()
        for first, second in combinations(clauses, 2):
            for resolvent in resolve(first, second):
                if not resolvent:
                    return True
                new.add(frozenset(resolvent))
        if new <= clauses:
            return False
        clauses |= new


kb = [frozenset({"~P", "Q"}), frozenset({"~Q", "R"}), frozenset({"P"})]
print(refutes(kb + [frozenset({"~R"})]))
print(refutes(kb + [frozenset({"~S"})]))

Output

True
False

Example details

Follow the code

Open the walkthrough to inspect the example one step at a time.

Show guided walkthrough

Guided walkthroughReady

1from itertools import combinations

4def negate(literal):

5 return literal[1:] if literal.startswith("~") else "~" + literal

8def resolve(first, second):

9 return [(first - {lit}) | (second - {negate(lit)}) for lit in first if negate(lit) in second]

12def refutes(clauses):

13 clauses = set(clauses)

14 while True:

15 new = set()

16 for first, second in combinations(clauses, 2):

17 for resolvent in resolve(first, second):

18 if not resolvent:

19 return True

20 new.add(frozenset(resolvent))

21 if new <= clauses:

22 return False

23 clauses |= new

26kb = [frozenset({"~P", "Q"}), frozenset({"~Q", "R"}), frozenset({"P"})]

27print(refutes(kb + [frozenset({"~R"})]))

28print(refutes(kb + [frozenset({"~S"})]))

Follow the example

Start to inspect the source, values, and output. These prepared steps explain the published sample; grouped loop steps describe multiple iterations.

View the complete dry-run table

Prepared trace of the published program. Some rows group repeated iterations.
What happens	State after step	Output so far
Resolution removes a literal from one clause and its complement from the other, and merges what remains.	`—`	—
An empty resolvent is a contradiction: no literal is left that could be true.	`—`	—
If a full round produces no new clause, the set is saturated and no contradiction exists.	`—`	—
Adding ¬R: P and ¬P ∨ Q give Q, then ¬Q ∨ R gives R, which clashes with ¬R. The empty clause appears, so KB entails R.	`—`	True
S does not appear in the knowledge base, so refutation fails: KB does not entail S.	`—`	True False

Behind the scenes

How Python processes this code

Python runs this source through its interpreter. It creates objects for values and resolves names as each statement runs.

Cost and common mistakes

The number of distinct clauses over n symbols can reach 3ⁿ, so the worst case is exponential. Strategies make typical problems far more tractable.

To prove Q, you must add the negation of Q, not Q. Adding the wrong sentence proves nothing.
Resolving on more than one complementary pair at once is not valid. Resolve one pair at a time.
Saturating the clause set can create exponentially many clauses. Real provers use strategies such as unit preference and set of support to limit that.

Try it yourself

Resolve the clauses {~P, Q} and {P} and name the result.

Reveal answer and reasoning

Resolving on P gives {Q}. This is how modus ponens appears in clause form.