While a refutation has not been found Copy two clauses from the set Generate all logical consequences, e.g., by resolution Put logical consequences into the setNote the "Copy", indicating that a clause may be used multiple times with a new set of variables each time.
Example | ||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
S = { wise(jim), ~wise(X) | wise(brother_of(X)), ~wise(brother_of(brother_of(jim))) }
|
Example | |||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
S = { p(f(X)) | q(Y), ~p(X) | q(dog), p(f(dog)) | ~q(X), ~p(f(Z)) }
|
Example |
---|
A = { ∀X (p(X) => (q(X) | r(X))), p(a) | p(b), ∀Y ~q(Y) } C = ∃X r(X) |
Full resolution is refutation complete for general clauses [Robinson 1965], and binary resolution is refutation complete for Horn clauses [Henschen & Wos 1974]. This means that if the input set is unsatisfiable, then the empty clause can always be derived in this manner, given infinite time and memory (i.e., resolution is theoretically refutation complete, practically incomplete). Such a deduction is called a refutation. If the input set is satisfiable, the resolution procedure may continue for ever.
Example (showing that binary resolution is not refutation complete) | |||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
S = { p(X) | q(Y) | q(X) ~q(a) | ~q(Z), ~p(a) }
|
A refutation can be represented as a proof tree.
Example | |||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
S2 = { ~p(X) | q(X) | r(X), p(a) | p(b), ~q(Y), ~r(a), ~r(b) }
|
This refutation has the proof tree :
Notice that the clause ~p(X) | r(X) is used twice in the proof tree but is generated only once by resolution.
A failure tree for an unsatisfiable set of clauses is a minimal finite subtree of the semantic tree of the Herbrand base, such that for each branch there is a clause that is FALSE in the sub-interpretation identified by that branch. FALSE has a single node as its failure tree.
Example |
---|
S = { wise(jim), ~wise(X) | wise(brother_of(X)), ~wise(brother_of(brother_of(jim))) } |
This unsatisfiable clause set has the failure tree :
Example |
---|
S = { p(a) | q(X), ~p(Y) | q(f(Y)), p(a) | ~q(T), ~p(A) | ~q(W) } |
A (Herbrand) unsatisfiable set of clauses has a failure tree
Proof |
---|
If a set of clauses is (Herbrand) unsatisfiable then for each branch of a fair semantic tree of the Herbrand base, i.e., for each Herbrand interpretation, there exists a clause in the set which has a ground instance that is FALSE in the Herbrand interpretation identified by that branch. As there are only a finite number of literals in each clause, and each literal has finite depth, each branch has a smallest sub-branch such that the truth value of the corresponding clause instance is determined by the sub-interpretation identified by the sub-branch. The leaf of such a sub-branch is called a failure node for the clause. The sub-branches define a finite sub-tree of the semantic tree. Prune any descendants of failure nodes to form a minimal sub-tree, i.e. a failure tree. |
Failures trees are used in the proofs of Herbrand's theorem and the completeness of resolution.
Proof |
---|
For a set of clauses S, let R(S) mean S ∪ {all resolvants from S}, and Rn(S) mean R applied n times. If S is (Herbrand) unsatisfiable, then it needs to be shown that there exists n such that FALSE is an element of Rn(S). If S is unsatisfiable, then it has a failure tree. If the tree is trivial, then FALSE is an element of S. Otherwise:
Note that the failure tree has a maximal depth equal to the size of the Herbrand Base, i.e., infinite. Thus the number of resolutions that might be necessary is the same. |
Example |
The failure tree for:
S = { wise(jim), ~wise(X) | wise(brother_of(X)), ~wise(brother_of(brother_of(jim))) }is
S = { wise(jim), ~wise(X) | wise(brother_of(X)), ~wise(brother_of(brother_of(jim))), ~wise(brother_of(jim)) }is
|
To show that C is a logical consequence of A, it is necessary to:
S' is unsatisfiable iff S = CNF(S') is unsatisfiable
A set of clauses has a model iff it has a Herbrand model, so
If a set S ∪ {a resolvant from S} of clauses is Herbrand unsatisfiable, then S is Herbrand unsatisfiable, so
The resolution procedure is refutation complete, so
~p(X) | q(X) | r(X) | + | ~q(Y) | » | ~p(X) | r(X) |
~p(X) | r(X) | + | ~r(a) | » | ~p(a) |
+ | ~r(b) | » | ~p(b) | |
~p(a) | + | p(a) | p(b) | » | p(b) |
p(b) | + | ~p(b) | » | FALSE |
S = { p(f(X)) | q(Y), ~p(X) | q(dog), p(f(dog)) | ~q(X), ~p(f(Z)) }