1
$\begingroup$

I was referring to this MIT OCW slides to learn about resolution refutation.

Recently I came across following problem:

Check if following is tautology

$(a\leftrightarrow c)\rightarrow (\lnot b\rightarrow (a\land c))$

I tried solving like this:

Premise:

$a↔c=(a∧c)∨(¬a∧¬c)$

$=(a∨¬a)∧(a∨¬c)∧(c∨¬a)∧(c∨¬c)$

$= (a∨¬c)∧(c∨¬a)$…this is CNF

Conclusion:

$¬(¬b→(a∧c))$

$=¬(b∨(a∧c))$

$=¬((b∨c)∧(b∨a))$

$=¬(b∨c)∨¬(b∨a)$

$=(¬b∧¬c)∨(¬b∧¬a)$

$=(¬b∨¬b)∧(¬b∨¬a)∧(¬c∨¬b)∧(¬c∨¬a)$

$=¬b∧(¬b∨¬a)∧(¬c∨¬b)∧(¬c∨¬a)$ …this is CNF

Then applied resolution refutation as follows:

enter image description here

I am not able to reduce this to false, so I can say that the contradiction is true and the statement is not a tautology. Am I correct with this? Also I have following doubts

  1. The examples in the slides explains examples which involve single variable conclusions (like $Z$ and $P$), but not compound expressions involving as in case of above. So did I handled conclusion involving compound expression above correctly?

  2. Is it correct to use the expansion of biconditional as in case of premise ($a\leftrightarrow c$) above?

  3. The slides says that we can bring FALSE after applying resolution inference rule, it means the contradiction is false and the original statement is valid. But, the slides does not explain what to conclude if we can bring TRUE after applying resolution rule, does it mean that the contradiction is true? And hence the given statement if invalid / not tautology.

    Above by applying resolution inference rule to point (1) and (2), I can get TRUE, right? $(a\vee\neg c)\wedge(\neg a\vee c) = (\neg a\to \neg c)\wedge(\neg c\to \neg a)=(\neg a\to \neg a)=a\vee \neg a=TRUE$

    If yes, then the next question.

  4. Does that mean all premises involving biconditional (above TRUE is obtained from biconditional premise expressed as conjunction) leads to correct contradiction?
$\endgroup$
1
$\begingroup$

Your "conjecture" is correct; as you can verify with a truth assignment $v$ such that :

$v(a)=v(b)=v(c)=$f

we have : $v(a ↔ c)=$t and : $v(¬b→(a∧c))=$f and thus the conditional is f, i.e. the formula is not a tautology.


The Resolution method is suitable for telling whether a propositional formula is satisfiable.

If the formula $\mathcal A$ is unsatisfiable, then $\lnot \mathcal A$ is a tautology.

If the example of your question, being unable to derive the empty clause (i.e. a contradiction), we have shown that the formula is satisfiable [try with a truth assignement $v'$ such that $v'(a)=$t and $v'(c)=$f].

But from the fact that a formula $\mathcal A$ is satisfiable, does not follow that it is a tautology.

And this is the case of the example : the formula is satisfiable but not a tautology.


Regarding the "unpacking" of the bi-conditional, the simplest way is to unpack it as :

$(a \to c) \land (c \to a)$

that gets directly :

$(\lnot a \lor c) \land (\lnot c \lor a)$.

Regarding point 4 :

Does that mean all premises involving biconditional leads to correct contradiction?

I'm not sure to understand it. If you are saying that all formulae involving a bi-conditional are satisfiable, this is clearly not true. Consider e.g. .

$(a ↔ c) \land a \land \lnot c$.


Resolution is also called "Resolution by refutation", because it is essentially a proof by contradiction; we have to start negating the desired conclusion, i.e asserting that the thing that we're trying to prove is false, and then we try to derive a contradiction.

We apply the Resolution rule until either we can derive "false" (the empty clause): if we assert that the negation of the thing that we're interested in is true, and then we derive a contradiciton, then we've succeeded in a proof by contradiction.

Resolution is a sound and complete proof procedure; for details, see :

We call resolution expansion for for $\{ X \}$a sequence of application of the resolution rule starting with the formula $X$.

Definition 3.3.4 We call a resolution expansion containing the empty clause closed.

Definition 3.3.5 A resolution proof of $X$ is a closed resolution expansion for $\{ \lnot X \}$. $X$ is a theorem of the resolution system if $X$ has a resolution proof.

Theorem 3.4.8 (Propositional Resolution Soundness) If $X$ has a resolution proof, then $X$ is a tautology.

Using Hintikka's Lemma (every propositional Hintikka set is satisfiable), it is possible to prove the (Propositional) Model Existence Theorem : every resolution expansion that is not closed can be embedded into a (propositional) Hintikka set, and thus it is saisfiable.

Finally :

Theorem 3.7.9 (Completeness for Propositional Resolution) If $X$ is a tautology, $X$ has a resolution proof.

Proof. If $X$ does not have a resolution proof, there is no closed resolution expansion for $\{ \lnot X \}$. Then $\{ \lnot X \}$ is satisfiable by the Model Existence Theorem; so $X$ is not a tautology.

$\endgroup$
  • $\begingroup$ ok I get that (1) if the formula $A$ is unsatisfiable, then $\lnot A$ is a tautology and (2) if the formula $A$ is satisifable, it does not follows that it is tautology. However is it like "if while using resolution approach, being unable to derive the empty clause, we have shown that the formula is satisfiable". When fail to derive empty clause, it can very well be unsatisifiable also, right? $\endgroup$ – anir123 Dec 31 '15 at 14:03
  • $\begingroup$ @PardonMeForMySuperPoorMaths - No; if - having correctly applied the resolution procedure until you reached a point where you cannot apply again the rule - you have not generated the empty clause, the formula must be satisfiable. The aim of the resolution procedure is to generate a contradiction; if no contradiction arises, the starting point (can be one or more formuale) is satisfiable. $\endgroup$ – Mauro ALLEGRANZA Dec 31 '15 at 14:07
  • $\begingroup$ I understand the aim of resolution procedure. But how failure to derive empty clause after correct application of resolution rule implies that " the statement must be satisfiable " Or I may ask why it cannot be unsatisfiable after failure to derive empty clause? $\endgroup$ – anir123 Dec 31 '15 at 21:13

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.