Using Resolution to Prove Theorems
- The first step to use resolution as a rule of inference we have to convert wffs into clauses.
- If ∆ |== w then set of clauses are also logically entailed from ∆.
- Resolution refutation can be used to prove a wff w from ∆.
- The first step is to negate w, and this negation is converted to clause form and this is added to clause form of ∆.
- Until we deduce an empty clause the resolution is applied.
- Let us consider the courier delivery robot. Let the couriers delivered to room 20 are smaller than any of the ones in 27. It can be denoted as
- (∀x, y) {[Courier(x) ∧ Courier(y) ∧ Inroom(x, 20) ∧ Inroom(27)] ⊃ Smaller(x, y)
- Converting the above wff into clause form and denoting Courier as C and Inroom as I and smaller as S we have,
- ᆨC(x) ∨ ᆨC(y) '.' ᆨI(x, 20) ∨ ᆨ(x, 27) ∨ S(x, y)
- If the robot knows the Courier B is in either of the rooms it can't know which is smaller. But it knows that A is in room 20 and A is not smaller than Courier B.
- C(B)
- C(A),
- I(B, 20)∨ I(B, 27).
- I(A, 20).
- ᆨS(A, B).
Now the robot which knows this information can prove that B is in room 20. By starting with the expression that B should not be in 20 the proof continues. It is shown in Figure.
Fig. A Resolution Refutation
The information i.e. wffs known to the robot are present at the right side of the Figure and which has to be proved i.e. B is not in room 20 is shown at the left hand side.
