Propositional resolution: the correct way to proceed

Question

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:

1. from 1 and 2 comes out ($\neg$L, H)$_{5}$;

2. from 5 and 4 comes out ($\neg$L, $\neg$V)$_{6}$;

3. from 2 and 6 comes out ($\neg$L)$_{7}$ and so
4. 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)?

Answer 1

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)?

It is a correct way.   There are others and its not easy to say which is the best way.   For myself, I'd start with statement three, the "smallest" clause, and progressively shrink the others

$$\begin{align} &~\{ (\neg L,\neg V,H )_{1}, (\neg L,V )_{2}, ( L )_{3}, (\neg V,\neg H )_{4} \} \\ ~& ~\{\color{grey}{(L)_3}, (\neg V, \neg H)_{4}, (\neg V, H )_{5}, (V)_{6}\} & \because \{1, 2\}\vdash 5, \{2, 3\}\vdash 6 \\ ~&~\{\color{grey}{(L)_3, (V)_{6}},(\neg H)_{7}, (H)_{8}\} & \because \{4,6\}\vdash 7, \{5,6\}\vdash 8 \\ ~&~ \{\} & \because \{7,8\}\vdash \bot \\ \therefore ~&~ \{ (\neg L,\neg V,H )_{1}, (\neg L,V )_{2}, ( L )_{3}\}\vdash \{(V),(H)\}\end{align}$$

---

PS: hopefully you noticed that $( L \wedge V) \leftrightarrow H$ is $(\neg L\vee \neg V\vee H)\wedge(\neg H\vee(L\wedge V))$ and so the clausal form of $F$ is: $$F=\{(\neg L, \neg V, H)_{1},(\neg H, L)_{1.1},(\neg H, V)_{1.2}, (\neg L,V )_{2}, ( L )_{3}\}$$

You just used a weakened form.