# Prove via predicate logic and the resolution

**"If a course is easy, there are somestudents that are enrolled in it who are happy"**

First Put into First Order form

∀c,easy(c)->∃s,happy(s)

now skolemize

∀c,easy(c)->happy(f(c))

next step dropping universal qunatifier

easy(c)->happy(f(c))

Eliminating Implication

¬easy(c) V happy(f(c))

Next part

**If a course has a final,no students that are enrolled in it are happy. ".**

Similarly

Put into first order form

∀c,final(c)->∃s,happy(s)

moving negation inward

∀c,final(c)->∀s,¬happy(s)

moving quantifiers outward

∀c,∀s,final(c)->¬happy(s)

Dropping universal quantifier

final(c)->¬happy(s)

Eliminating implication

¬final(c)->¬happy(s)

Therefore we have 2 clauses

**1)¬easy(c) V happy(f(c))**

**2)¬final(k)->¬happy(s)**

Now we need to prove

**“If a course has a final, the course isnot easy”**

Putting into first order form

∀c,final(c)->¬easy(c)

dropping universal quantifier

final(c)->¬easy(c)

Eliminating implication

¬final(c) V ¬easy(c)

renaming the variable to avoid conflicts in the clauses

¬final(j) V ¬easy(j)

for resolution we need to negat the clauses we are trying to prove

final(j) ∧ easy(j)

Lets complete caluses set tat the start of resolutions look like

A)

¬easy(c) V happy(f(c))

B)

¬final(k) V ¬happy(s)

C)

final(j)

D)

easy(j)

**Resolution**

Combining A & D with the resolution will get

E)

happy(f(c))

Combining B & C witht the resolution will get

¬happy(s)

Combining E & F witht the resolution will get

Ø

Intuitively E & F is contradicting each other

E stating that a particular student

f(c) is happy while F stating that no student is happy

therefore

we have derived contradiction by assuming the negation of

¬final(j) V ¬easy(j)

ex/Consider the following information: "The outcome of a coin toss must be head or tails. Heads I win, tails you lose. If you lose then I win and, if I win then you lose". Convert the above knowledge into propositional logic then prove using the resolution method that "I win."

sol//

**Statement (1): The outcome of a coin toss must be head or tails****Prepositional logic:**- Here is logical OR connective which represents either or.
**Statement (2): Heads I win.****Meaning =>**If Head is the outcome then I will win.**Prepositional logic:**- Here represents if-then statement.
**Statement (3): tails you lose.****Meaning =>**If Tail is the outcome then You will lose.**Prepositional logic:**- Here represents if-then statement.
**Statement (4): If you lose then I win.****Prepositional logic:**- Here represents if-then statement.
**Statement (5): If I win then you lose.****Prepositional logic:**- Here represents if-then statement.

**Proof using resolution that I win:**

**Step(1): Eliminate all the implications symbols () using following formula :**

**Statement (1):**- No need to convert as the statement don't have implication sign.
**Statement (2):**- Conversion :
**Statement (3):**- Conversion :
**Statement (4):**- Conversion:
**Statement (5):**- Conversion:

"No food made by Cadbury’s is green."

C(x) means “x is a child.”

F(x) means “x is food.”

L(x, y) means “x likes y.”

G(x) means “x is green.”

M(x, y) means “x makes y.”

c means “Cadbury’s.”

Primises:

1. (∃x)(C(x) ∧ (∀y)(F(y)→L(x,y)))

2. (∀x)(C(x)→(∀y)((F(y) ∧ G(y))→¬L(x,y)))

3. (∀x)((F(x) ∧ M(c,x))→(∀y)(C(y)→L(y,x)))

Conclusion: (∀x)((F(x) ∧ M(c,x))→¬G(x))

First, negate the conclusion and add it to the set of premises

(∃x)(C(x) ∧ (∀y)(F(y)→L(x,y)))

∧ (∀x)(C(x)→(∀y)((F(y) ∧ G(y))→¬L(x,y)))

∧ (∀x)((F(x) ∧ M(c,x))→(∀y)(C(y)→L(y,x)))

∧ ¬ ((∀x)((F(x) ∧ M(c,x))→¬G(x)))

1. Some children will eat any food.

2. No children will eat food that is green.

3. All children like food made by Cadbury’s.

(∃x)(C(x) ∧ (∀y)(F(y)→L(x,y)))

∧ (∀x)(C(x)→(∀y)((F(y) ∧ G(y))→¬L(x,y)))

∧ (∀x)((F(x) ∧ M(c,x))→(∀y)(C(y)→L(y,x)))

∧ ¬ ((∀x)((F(x) ∧ M(c,x))→¬G(x)))

expression 1:

(∃x)(C(x) ∧ (∀y)(F(y)→L(x,y)))

‘→’ must be eliminated first:

(∃x)(C(x) ∧ (∀y)(¬F(y) ∨ L(x,y)))

bring the quantifiers to the front

(∃x)(∀y)(C(x) ∧ (¬F(y) ∨ L(x,y)))

skolemize, to eliminate the existential quantifier

(∀y)(C(a) ∧ (¬F(y) ∨ L(a,y)))

This can be expressed as the following clauses:

{C(a)}, {¬F(y), L(a,y)}

(∃x)(C(x) ∧ (∀y)(F(y)→L(x,y)))

∧ (∀x)(C(x)→(∀y)((F(y) ∧ G(y))→¬L(x,y)))

∧ (∀x)((F(x) ∧ M(c,x))→(∀y)(C(y)→L(y,x)))

∧ ¬ ((∀x)((F(x) ∧ M(c,x))→¬G(x)))

expression 2

(∀x)(C(x)→(∀y)((F(y) ∧ G(y))→¬L(x,y)))

→is eliminated first:

(∀x)(¬C(x) ∨ (∀y)(¬(F(y) ∧ G(y)) ∨ ¬L(x,y)))

Now DeMorgan’s law is applied:

(∀x)(¬C(x) ∨ (∀y)(¬F(y) ∨ ¬G(y) ∨ ¬L(x,y)))

Quantifiers are moved to the front:

(∀x)(∀y)(¬C(x) ∨ ¬F(y) ∨ ¬G(y) ∨ ¬L(x,y))

ex/Convert the following sentences into their corresponding Clause form (CNF):

1- There is a cub on top of every red cylinder.2- Every city has a dogcatcher who has been bitten by every dog in town.

3- It is raining, but there is no rainbow.