Prove via predicate logic and the resolution

ex/Consider the following information: "If a course is easy, there are some students that are enrolled in it who are happy. If a course has a final exam, no students that are enrolled in it are happy. ". Prove via predicate logic and the resolution method that: “If a course has a final exam, the course is not easy”.

sol//

"If a course is easy, there are some
students 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 is
not 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: 
• 
  
  
  
  

ex/Consider the following information: "The humidity is high or the sky is cloudy. If the sky is cloudy then it will rain. If the humidity is high then it is hot. It is not hot." Convert them into Propositional Logic formula then use resolution to prove: "It will rain."

sol//

ex/Consider the following: "Some children will eat any food. No children will eat food that is green.

All children like food made by Cadbury’s". Prove using predicate logic and resolution that:
"No food made by Cadbury’s is green."

sol//

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.

sol//

ex/Consider the following information: "If X is on top of Y then Y supports X. If X is above Y and they are touching each other then X is on top of Y. A cup is above a book. A cup is touching a book". Prove via predicate logic and the resolution method that: "the book supports the cup".

sol//

تعديل المقال