1

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.

Aadi Droid
  • 147

2 Answers2

3

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.

Mauro ALLEGRANZA
  • 94,169
  • I am familiar with the method where a ψ is mentioned, my problem I have no explicit ψ mentioned! I just have about 10 ϕ and I am supposed to do resolution refutation! – Aadi Droid Oct 04 '14 at 15:12
  • @AadiDroid - Ok: apply definition : "resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic. In other words, iteratively applying the resolution rule in a suitable way allows for telling whether a propositional formula is satisfiable and for proving that a first-order formula is unsatisfiable." Apply it to $ϕ1∧ϕ_2∧…∧ϕ{10}$ to prove that it is satisfiable or not ... – Mauro ALLEGRANZA Oct 04 '14 at 15:57
  • That makes sense, and that is what i've been trying to do for a couple of days now. I am running into loops. Is it safe to negate one of the statements and then apply the rules to lead to a box? – Aadi Droid Oct 04 '14 at 16:20
  • @AadiDroid - as per the first answer : "it would be recommend to see the whole question"... Having said that, the set initial $S$ of statements is what it is. If applying resolution you will end with a set $S'$ which do not include the empty clause, $S'$, and so also the original $S$, is satisfiable. – Mauro ALLEGRANZA Oct 04 '14 at 16:57
  • You can see here a simple example ... – Mauro ALLEGRANZA Oct 04 '14 at 17:00
0

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!

Bruno Bentzen
  • 3,362