Predicate-calculus Resolution
- If r1 is a clause and ф is an atom in it and r2 is a clause with a literal ᆨψ in it.
- These ф and r have a mgu μ then there will a resolvent P obtained by substituting μ in union of r1 and r2 the complementary literals are left. That is,
- P = [(r1 - {Ñ„}) ∪ (r2 ー {ᆨψ})]μ
- The variables in the different clauses are renamed before applying resolution.
- Example: To resolve,
- P(y) ∨ Q(f(y)] and
- R(g (y)) ∨ ᆨQ(f(A))
- The first to apply resolution we have to change the variables in one of the clause so we change in second one to get R(g(z)) ∨ ᆨQ(f(A))
- Applying resolution we get, P(A) ∨ Q(g(z))
- Standardizing the Variables Apart: It is a process of renaming the variables.
- Example: {P(y, y), Q(y), R(y)} and {ᆨP(A, x), ᆨQ(B)} this can be resolved in two ways and produces {Q(A), R(A), ᆨQ(B)} and {P(B, B), R(b), ᆨ(A, x)}.
- If there are two clauses like {Q(u), Q(v)} and {ᆨQ(x), ᆨQ(y)} which have their ground instances equivalent to Q(B) and ᆨQ(B) from which we can infer empty clause.
- To infer these empty clause from original clauses we use stronger resolution rule.
- That is, If r1 and r2 are two clauses and r'1 and r'2 are subsets of them so that these r'1 literals can be unified with negations of r'2 literals with mgu μ then they have a resolvent p.
- p is obtain by substituting μ is union of r1 and r2 by not considering the complementary subsets.
- ∴ p[(r1 – r'1) ∪ (r2 – r'2)] μ
- By using the definition above {Q(u), Q(v)} and ᆨP(x), ᆨP(y)} can be resolved to product an empty clause.
Completeness and Soundness
- The resolution that is used in predicate calculus is sound.
- The soundness of predicate calculus is stated by saying that if the resolvent of two clauses ф and ψ is p, then (ф, ψ) |== p.
- Completeness of resolution is complicated as all the formulas which are logically entailed by a given set cannot be inferred by resolution.
- Example: Q(A) ∨ Q(B) cannot be inferred from P(A).
- Stronger rule of resolution can be used to guarantee refutation completeness.
