- #1
Agaton
- 26
- 0
I need help with the following question on Resolution in FOL.
The custom officials searched everyone who entered this country who was not a VIP. Some of the drug pushers entered this country and they were only searched by drug pushers. No drug pushers was a VIP. Let E(x) mean ”x entered this country”, V (x) mean ”x was a VIP, S(x, y) mean ”y searched x”, C(x) mean ”x was a custom official”, and P(x) mean ”x was a drug pusher”. Use these predicates to express the above statements in first order logic. Conclude by resolution that some of the officials were drug pushers.
I translated the sentences as follows:
1.The custom officials searched everyone who entered this country who was not a VIP
∀x (E(x) /\ ¬V(x)) ----> ∃y (C(y) /\ S(x,y)
2. Some of the drug pushers entered this country and they were only searched by drug pushers.
∃x (P(x) /\ E(x)) /\ ∃y (S(x,y) /\ P(y)
3. No drug pushers was a VIP
∀x V(x) ---> ¬P(x)
4. some of the officials were drug pushers(conclusion)
∃x C(x) /\ P(x)
The next step, as long as I know, is to convert the above sentences one by one to CNF, and remover the quantifiers. I try for each sentence:
a) First i need to remove the implication:
Sentence1. ∀x (E(x) /\ ¬V(x)) ----> ∃y (C(y) /\ S(x,y)
a) First i need to remove the implication:
∀x ¬(E(x) /\ ¬V(x)) \/ ∃y (C(y) /\ S(x,y)
∀x (¬E(x) /\ V(x)) \/ ∃y (C(y) /\ S(x,y) //by Implication elimination
b) Now I need to remove the quantifiers by introducing constants:
(¬E(P) /\ V(P)) \/ ∃y (C(Q) /\ S(P,Q) //Not sure at all ...
c) now i need to convert to CNF, but instead i have DNF, disjunction of two sentence.
Sentence 2. ∃x (P(x) /\ E(x)) /\ ∃y (S(x,y) /\ P(y)
a) what i need is to remove existential, but i am really not sure.
Sentence 3. ∀x V(x) ---> ¬P(x)
a) ∀x ¬ V(x) \/ P(x) // Implication elimination
b) again existential elimination which i don't know how...
sentence 4. ∃x C(x) /\ P(x)
a) existential elimination is required...
I really appreciate any help to convert these sentences to conjunctive normal form and quantifier elimination, in order to so the last step, resolution.
Thanks in advance.
The custom officials searched everyone who entered this country who was not a VIP. Some of the drug pushers entered this country and they were only searched by drug pushers. No drug pushers was a VIP. Let E(x) mean ”x entered this country”, V (x) mean ”x was a VIP, S(x, y) mean ”y searched x”, C(x) mean ”x was a custom official”, and P(x) mean ”x was a drug pusher”. Use these predicates to express the above statements in first order logic. Conclude by resolution that some of the officials were drug pushers.
I translated the sentences as follows:
1.The custom officials searched everyone who entered this country who was not a VIP
∀x (E(x) /\ ¬V(x)) ----> ∃y (C(y) /\ S(x,y)
2. Some of the drug pushers entered this country and they were only searched by drug pushers.
∃x (P(x) /\ E(x)) /\ ∃y (S(x,y) /\ P(y)
3. No drug pushers was a VIP
∀x V(x) ---> ¬P(x)
4. some of the officials were drug pushers(conclusion)
∃x C(x) /\ P(x)
The next step, as long as I know, is to convert the above sentences one by one to CNF, and remover the quantifiers. I try for each sentence:
a) First i need to remove the implication:
Sentence1. ∀x (E(x) /\ ¬V(x)) ----> ∃y (C(y) /\ S(x,y)
a) First i need to remove the implication:
∀x ¬(E(x) /\ ¬V(x)) \/ ∃y (C(y) /\ S(x,y)
∀x (¬E(x) /\ V(x)) \/ ∃y (C(y) /\ S(x,y) //by Implication elimination
b) Now I need to remove the quantifiers by introducing constants:
(¬E(P) /\ V(P)) \/ ∃y (C(Q) /\ S(P,Q) //Not sure at all ...
c) now i need to convert to CNF, but instead i have DNF, disjunction of two sentence.
Sentence 2. ∃x (P(x) /\ E(x)) /\ ∃y (S(x,y) /\ P(y)
a) what i need is to remove existential, but i am really not sure.
Sentence 3. ∀x V(x) ---> ¬P(x)
a) ∀x ¬ V(x) \/ P(x) // Implication elimination
b) again existential elimination which i don't know how...
sentence 4. ∃x C(x) /\ P(x)
a) existential elimination is required...
I really appreciate any help to convert these sentences to conjunctive normal form and quantifier elimination, in order to so the last step, resolution.
Thanks in advance.