# Proof using Resolution Refutation?

I have this question and an answer I attempted below. I would like to know if I did this question properly since I don't know anyway I can check my answer online. Thanks!

Question:

Consider the following scenario: “Bob has money. The car is silver. The car is fast. If the car is silver or if the car is fast, and Bob has money then Bob goes on vacation on a cruise.”

• Oh, my bad I forgot to change the numbering. Nonetheless, thanks for all your help. Wouldn't have understood either of these question without you.
– name
Feb 20, 2017 at 23:53

I think you haven't grasp the procedure...

You have the scenario :

“Bob has money. The car is silver. The car is fast. If the car is silver or if the car is fast, and Bob has money then Bob goes on vacation on a cruise.”

Formalize and prove or disprove this claim: Bob goes on vacation on a cruise.

First, you have to list the premises (following your symbolization):

$A, B, C, [(B \lor C) \land A] \to D$

and the sought conclusion: $D$.

To prove that $D$ is entailed by the premises we have to list all the premises and the negation of the conclusion :

1) $A$

2) $B$

3) $C$

4) $[(B \lor C) \land A] \to D$

5) $\lnot D$

The further step needed is to rewrite 4) as a CNF:

4') $(¬A \lor ¬B \lor D) \land (¬A \lor ¬C \lor D)$.

In the end, we have to apply the Resolution procedure to the following clauses:

1) $A$

2) $B$

3) $C$

4a) $¬A \lor ¬B \lor D$

4b) $¬A \lor ¬C \lor D$

5) $\lnot D$.

Related to your previous post, this is $F$: the "initial" set of clauses.

Firstly, we have to produce $Res(F) = F \cup \{ \text { all the resolvents of clauses of } F \}$.

The resolvants are :

6) $¬B \lor D$ --- from 1) and 4a)

7) $¬C \lor D$ --- from 1) and 4b)

8) $¬A \lor D$ --- from 2) and 4a

9) $¬A \lor D$ --- from 3) and 4b)

10) $¬A \lor ¬D$ --- from 5) and 4a

11) $¬A \lor ¬C$ --- from 5) and 4b

of course deleting the repeted formulae.

And so on...

• Oh.... I forgot to include the statements as premises/facts. May you checked my edited answer. Thanks!
– name
Feb 20, 2017 at 11:08
• Also, thanks for the clarification on the previous question, I now understand that. I don't know if you saw my other comment, but if you may check my edited answer that will be great. Thanks!
– name
Feb 20, 2017 at 16:15