Resolution Refutation

Question

I am solving a few questions to better understand the way resolution works and now i've come across this question which has no explicit conclusion and I am supposed to use 'Resolution Refutation' to a set of clauses! I am having difficulty understanding what exactly this means, is it ok to choose any of the clauses and negate them and then try to arrive at a contradiction?

Posting the whole question here can be perceived as posting a homework and so I am not doing it.

Answer 1

In general, the Resolution method amounts to prove that a set $\{ ϕ_1,ϕ_2,\ldots, ϕ_n \}$ of formulae logically imply a formula $\psi$, or equivalently that the sentence :

(1) $\quad \vDash ϕ_1 \land ϕ_2 \land \ldots \land ϕ_n \rightarrow \psi$ is valid,

showing that the set $\{ ϕ_1,ϕ_2,\ldots, ϕ_n, \lnot \psi \}$ is unsatisfiable.

Th method needs that the sentence (1) is transformed into a conjunctive normal form with the conjuncts viewed as elements in a set $S$ of clauses.

---

We can also apply the method to a set $\{ ϕ_1,ϕ_2,\ldots, ϕ_n \}$ of formulae to show that it is satisfiable or not.

If the application of the method derives the empty clause, then we can conclude that the set is unsatisfiable, which is equivalent to say that :

$ϕ_1 \land ϕ_2 \land \ldots \land ϕ_{n-1} \rightarrow \lnot ϕ_n$ is valid.

Answer 2

I would recommend you to post the whole question, so we can understand the.conext of your problem. However, as you posted it, I would rather bet you are requested to use the resolution method, i.e. verify whether one of the formulae $\phi_1, \phi_2, ... \phi_n$ in a formulae of the form $\phi_1\wedge \phi_2 \wedge ... \wedge \phi_n$ is false.

Obviously not every formula is given so. Fortunatelly we have algebraic manipulations techniques to provide its convertion to its conjunctive normal form, such that every $\phi_i$ stands for a propositional letter $p_i$ or its negation $\neg p_i$. The classic example are the distributivity property, De Morgan laws and so, that you probably know well.

Good work!