Created on March 6, 2013, 3:03 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:35 p.m.
The Resolution technique/method for automatic deduction of a Tautology or a Contradiction, i.e. how to proof that a Knowledge Base is correct or that and Implication is correct or how to proof that a Fact is implied or entailed by a given Knowledge Base. While Resolution for Propositional Logic is simple, for First Order Logic it gets a little bit more complicated because here one has Variables and Functions inside Clauses or Canonical Normal Forms.
Assuming two Clauses contain Variables and Functions, they trouble is how can one identify Literals that are negated or not negated and then resolute them via an Resolution Step and identify beforehand. However, this is complicated. What one can do is to do Substitutes, which means that one for example can substitute Variables by Constants and also substitute Variables with Functions of Variables.
In the following example one can achieve a Resolution by Substituting the Variable X with the Constant a and secondly one can substitute the Variable Z with a Function of the Variable Y, i.e. f of Y. With these Substitutions one can make a Resolution, because a part in both Clauses can be removed. Of course also in the remaining parts of the Clauses the Substations have to be applied. So the result also changes. So f of X will become f of a and Z will become r of Y.
In general this technique is called Substitution or Unification to identify possibilities where one can apply Resolution in First Order Logic.
The Unification of Terms is defined in the following way. Assuming one has two Literals L1 and L2 and what one wants is a Variable Substitution σ. So Variables can be substituted by Variables or Functions of Variables. This Variable Substitution σ should be applied with L1 and L2, i.e. the two Literals. The result should be that L1 and the Substitution it is equal and L2 with the applied Substitution. If there is such a Variable Substitution σ, then σ is a Unifier of the Literals L1 and L2. This is mandatory as the Variable on wants to substitute
The Unification Algorithm works in the following way. Given two Literals L1 and L2 one is looking for a Unifier σ for L1 and L2. One has to consider several Cases. First case is that L1 and L2 are both Constants, then they are only unifiable if L1 and L2 are really the same, i.e. they are equal. Otherwise one can not do a Variable Substitution. If L1 is a Variable and L2 is an arbitrary Term, then they are unifiable if for Variable L1 the Term L2 can be substituted and Variable L1 does not occur in Variable L2, then the Variable must not occur in the Term L2. Otherwise it is not unifiable. The third case to consider is that if L1 and L2 are Predicates or Functions. For example, Predicate L1 and L2 have the arguments s1 to sm and t1 to tm, respectively, are only unifiable if the are really the same or the Arity of both is the same, i.e. m is the same as n and all the terms si and ti must be unifiable, which means that si must be unifiable with he term ti. Only then, both are unifiable.
For Resolution in First Order Logic additional Variable Bindings have to be considered with the help of Substitutions
e.g. ( p(X,f(Y))) ∨ q(f(X),Y)) (¬p(a,Z) ∨ r(Z) )
Substitutions: Resolution with [X/a, Z/f(Y)] results in (q(f(a),Y) ∨ r(f(Y)).
Unification of Terms
Unification Algorithm - Given: Literals L1, L2 - Wanted: Unifier σ of L1 and L2
L1 and L2 are Constants: only unifiable, if L1 = L2.
L1 is Variable and L2 arbitrary Term: unifiable, if for Variable L1 the Term L2 can be substituted and Variable L1 does not occur in L2.
L1 and L2 are Predicates or Functions
PL1(S1 ,..., Sm) and PL2(t1,...,tn):
unifiable, if
Examples of Unification
L1 | L2 | σ |
p(X,X) | p(a,a) | [X/a] |
p(X,X) | p(a,b) | n.a. |
p(X,Y) | p(a,b) | [X/a, Y/b] |
p(X,Y) | p(a,a) | [X/a, Y/a] |
p(f(X),b) | p(f(c),Z) | [X/c, Z/b] |
p(X,f(X)) | p(Y,Z) | [X/Y, Z/f(Y)] |
p(X,f(X)) | p(Y,Y) | n.a. |
For example given a Knowledge Base split in Terminological and Assertional Knowledge. In the Tbox it is define that a human always has a parent and one defines what a orphan is which is of course a human who's parents are not alive anymore.
In the Assertional Knowledge Base, the Abox we say that Harry Potter is an orphan and that James Potter is a parent of Harry Potter. The question is given these Facts, whether it is possible to deduce that James Potter is not alive anymore.
For this one has to proof that the Knowledge base entails that James Potter is not alive. Thus, one has to proof that the knowledge Base implies that James Potter is not alive, so that this is a Tautology. TO do that with the Resolution one has to negate this Statement. So one has to proof that the Negation of that Statement should be a Contradiction. Then one has to transform this into the Canonical Form, i.e. the Clausal Form. On this Clauses one can apply Resolution for First Order Logic.
With the Knowledge Base one tries to find to Clauses that can be combined with a Resolution Step. For instance, a possible Resolution Step would be to take Clause number 3 and Clause number 7 with the Substitution that Variable X1 is replaced by Harry Potter and Variable Y1 is replaced by James Potter. If one does this with a Resolution Step one can remove the Predicate parent of, because one has it one time negated and one time not negated. So one can deduce from this Resolution that not orphan Harry Potter and not alive James Potter. This Fact is added to the knowledge Base. Next two new Clauses need to be found that can be combined. For example Clauses number 8 and number 9 can be combined, simply because it has the function alive and its not alive with the same Constant, i.e. the same Individual. So one do again a Resolution Step and the result will be not orphan Harry Potter, which is put into the Knowledge Base. Considering now the Clauses orphan Harry Potter and not orphan Harry Potter, if combined results in a Resolution Step into the empty Clause. So with this is was shown that the Knowledge Base is a Contradiction, which means on the other hand that the previous assumption of not negated Statement was a Tautology. So therefore one can deduce that James Potter is not alive.
So Resolution is a Method for the entailment of new facts from Knowledge Base
example for FOL Resolution:
Terminological Knowledge (TBox):
(∀X)( human(X) → (∃Y) parent_of(Y,X) ) (∀X)( orphan(X)) ↔ (human(X) ∧ ¬(∃Y) (parent_of(Y,X) ∧ alive(Y)))
Assertional Knowledge (ABox)
orphan(harrypotter) parent_of(jamespotter,harrypotter)
Can we deduce: ¬alive(jamespotter)?
We have to proof that it is a Tautology
¬((∀X)( human(X) → (∃Y) parent_of(Y,X) ) ∧ (∀X)( orphan(X)) ↔ (human(X) ∧ ¬(∃Y) (parent_of(Y,X) ∧ alive(Y))) ∧ orphan(harrypotter) ∧ parent_of(jamespotter,harrypotter)) → ¬alive(jamespotter))
(∀X)(∃X1)(∀X1)(∀Y1)(∀X2)(∃Y2) (( ¬human(X) ∨ parent_of(Y,X) ) ∧ (¬orphan(X1) ∨ human(X1) ∧ (¬parent_of(Y1,X1) ∨ ¬alive(Y1))) ∧ (orphan(X2) ∨ (¬human(X2) ¬ (parent_of(Y2,X2) ∧ alive(Y2))) ∧ orphan(harrypotter) ∧ parent_of(jamespotter,harrypotter)) ∧ alive(jamespotter))
Clausal Form (CNF):
( ¬human(X) ∨ parent_of(f(X), X) ) ∧ (¬orphan(X1) ∨ human(X1)) ∧ (¬orphan(X1) ∨ ¬parent_of(Y1,X1) ∨ ¬alive(Y1)) ∧ (orphan(X2)) ∨ ¬human(X2) ∨ parent_of(g(X,X1,Y1,X2),X2)) ∧ (orphan(X2)) ∨ ¬human(X2) ∨ alive(X,X1,Y1,X2))) ∧ orphan(harrypotter)) ∧ parent_of(jamespotter,harrypotter)) ∧ alive(jamespotter)
1. {¬human(X), parent_of(f(X),X)}, 2. {¬orphan(X1), human(X)}, 3. {¬orphan(X1),¬parent_of(Y1,X1),¬alive(Y1)}, 4. {orphan(X2),¬human(X2),parent_of(g(X,X1,Y1,X2),X2)}, 5. {orphan(X2),¬human(X2),alive(g(X,X1,Y1,X2))}, 6. {orphan(harrypotter)}, 7. {parent_of(jamespotter,harrypotter)}, 8. {alive(jamespotter)}
Entailed Clauses:
9. {¬orphan(harrypotter}, ¬alive(jamespotter)} (3,7)[X1/harrypotter, Y1/jamespotter] (3,7) 10. {¬orphan(harrypotter)} (8,9) 11. ⊥ (6,10)
Comment on This Data Unit