Question :
Consider the following sentences and prove that "Diana will win the game"
1.All Players are clever.
2.Anyone who is clever and dedicated can play the game well.
3.Anyone who is playing the game well will win his/her game.
4.Diana is a dedicated player.
So my first attempt was representing the using axioms and clausal form as follows(Please note that I'll be using the following notations as follows:
VX - For all X(Universal quantifier)
EX - For some X(Existential quantifier)
Let P(X) be X is a player
C(X) be X is clever
D(X) be X is dedicated
G(X) be X can play the game well
W(X) be X will win his/her game
Axiom Form :
1. VX [P(X) --> C(X) ]
2. [ ( C(X) ^ D(X) ) --> G(X) ]
3. VX [ G(X) --> W(X) ]
4. P(Diana) --> D(X)
Clausal Form :
1. ~P(X) v C(X)
2. ~C(X) v ~D(X) v G(X)
3. ~G(X) v W(X)
4. ~P(Diana) v D(X)
Can anyone guide me how to prove that "Diana will win the game" , using above clausal forms? Am I following the correct path displaying the above sentences in axioms and in clausal form?
Thanks!
To prove that "Diana will win the game" using the given clauses, you can use resolution refutation method, which involves negating the statement you want to prove and simplifying it by resolving it with the given clauses.
First, let's negate the statement "Diana will win the game":
~W(Diana)
Now, let's add this negated statement to the set of clauses:
1. ~P(X) v C(X)
2. ~C(X) v ~D(X) v G(X)
3. ~G(X) v W(X)
4. ~P(Diana) v D(X)
5. ~W(Diana) (negated statement)
To find a contradiction, we will try to resolve these statements. Here are the steps to follow:
1. Resolve clauses 3 and 5:
~G(X) v W(X) (3)
~W(Diana) (5)
---------------
~G(X) (resolvent)
2. Resolve clauses 4 and 1:
~P(Diana) v D(X) (4)
~P(X) v C(X) (1)
---------------
C(Diana) (resolvent)
3. Resolve clauses 2 and 5 (after renaming variables for clarity):
~C(A) v ~D(A) v G(A) (2)
~W(Diana) (5)
---------------
~C(Diana) v ~D(Diana) v G(Diana) (resolvent)
4. Resolve clauses 6 and 2:
~C(A) v ~D(A) v G(A) (2)
~C(Diana) v ~D(Diana) v G(Diana) (6)
---------------
~D(Diana) v G(A) v G(Diana) (resolvent)
5. Resolve clauses 3 and 7:
~G(X) (3)
~D(Diana) v G(A) v G(Diana) (7)
---------------
G(A) v G(Diana) (resolvent)
6. Resolve clauses 1 and 8:
~P(X) v C(X) (1)
G(A) v G(Diana) (8)
---------------
C(A) (resolvent)
Now, we have reached a contradiction with the statements 'C(A)' and '~C(A)'. Since we have a contradiction, we can conclude that our initial assumption (negation) is false, and therefore, "Diana will win the game" is true.
Therefore, using the resolution refutation method, we have proved that "Diana will win the game" based on the given clauses.