I'm trying to solve the following exercise:
using resolution, tell whether the following formula can be proven:
F = {( L $\wedge$ V) $\rightarrow$ H, L $\rightarrow$ V , L } entails (V $\wedge$ H).
I know that the propositional resolution procedure consists of proving that F $\wedge$ $\neg$ (V $\wedge$ H) is unsatisfiable, therefore I'm actually working on this set of clauses (in clausal normal form):
{ ($\neg$ L,$\neg$V,H )$_{1}$, ($\neg$ L,V )$_{2}$, ( L )$_{3}$, ($\neg$ V,$\neg$ H )$_{4}$ }.
My question comes out here indeed: is there an exactly way to keep pairs of clauses for resolving them? I mean, my opinion is that the following procedure is right:
from 1 and 2 comes out ($\neg$L, H)$_{5}$;
from 5 and 4 comes out ($\neg$L, $\neg$V)$_{6}$;
- from 2 and 6 comes out ($\neg$L)$_{7}$ and so
- from 3 and 7 comes out {} which means that F entails (V $\wedge$ H).
Is this a correct way to go or is there a precise way that I did not understand (about how considering the pair of clauses to solve)?