1
$\begingroup$

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

$\endgroup$
0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thank you Graham (there was a mistake in the initial text, I've just fixed it, excuse me). However I think I know. Now, just out of curiosity: it could be that by following a specific way, I will not able to show the unsatisfiability? I mean: let's suppose that there is no model that satisfies the formula above but obviously we don't know that. In this case: all ways bring me to the same conclusion (that is, the negation of F is unsatisfiable)? I think so because otherwise it would mean that the negation would be satisfiable (is a stupid question, I know but just to be sure). $\endgroup$ – Matteo May 12 '16 at 14:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.