Resolution and proof by refutation
Prove a conclusion by adding its negation to the clauses and deriving the empty clause.
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"})]))True False
Explanation
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.
Explore the dry run
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"})]))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
| Step / line | 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 |
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.