- #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.![Confused :confused: :confused:](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
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.