Resolution refutation with biconditional

Question

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:

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?

Answer 1

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 :

• Melvin Fitting, First-Order Logic and Automated Theorem Proving (1990), page 51-on.

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.