December 31st, 2010, 05:35 AM  #1 
Newbie Joined: Dec 2010 Posts: 11 Thanks: 0  Resolution in Predicate logic
I need help with the following question on Resolution in predicate logic: 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. Thanks in advance. 
December 31st, 2010, 06:05 AM  #2 
Senior Member Joined: Nov 2010 From: Staten Island, NY Posts: 152 Thanks: 0  Re: Resolution in Predicate logic
It's been a while since I did any of this, but here goes: (1) (2) (3) I don't know what the "formal rules" of resolution are, but the idea should be the following: Choose x satisfying (2), use the contrapositive of (3), and then apply to (1). 
December 31st, 2010, 02:56 PM  #3 
Newbie Joined: Dec 2010 Posts: 11 Thanks: 0  Re: Resolution in Predicate logic
Thank you very much for your answer. I first tried to translate the sentences to the language of FOL 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) Since I want to go through resolution, the next step, as long as I know, is to convert the above sentences one by one to Conjunction Normal form (CNF), and then remover the quantifiers, before doing resolution. I tried for each sentence, though it was quite unsuccessful: 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) //by Implication elimination ?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 if you please help me to convert them to CNF and removing quantifiers. 
January 1st, 2011, 09:31 AM  #4 
Senior Member Joined: Nov 2010 From: Staten Island, NY Posts: 152 Thanks: 0  Re: Resolution in Predicate logic
Let me try the first one for you: First of all is a logical axiom, so you can drop the initial Note that your second sentence is wrong (compare with mine in my first post). Hope this helps. 
January 1st, 2011, 03:56 PM  #5 
Newbie Joined: Dec 2010 Posts: 5 Thanks: 0  Re: Resolution in Predicate logic
Thanks a lot, that was quite helpful. Here is the above sentences converted to CNF: 1. (¬E(x) \/ V(x) \/ C(f(x))) /\ (¬E(x) \/ V(x) \/ S(x,f(x))) 2. P(a) /\ E(a) /\ (¬S(a,y) v P(y)) 3. ¬V(z) \/ P(z) 4. C(b) /\ P(b) The next step is to do resolution... 
January 2nd, 2011, 03:57 AM  #6 
Senior Member Joined: Nov 2010 From: Staten Island, NY Posts: 152 Thanks: 0  Re: Resolution in Predicate logic
Number 3 should be 3. ¬V(z) \/ ¬P(z) See if this helps. 
January 3rd, 2011, 05:38 AM  #7 
Newbie Joined: Dec 2010 Posts: 5 Thanks: 0  Re: Resolution in Predicate logic
DrSteve, thanks again.

January 3rd, 2011, 03:48 PM  #8 
Newbie Joined: Dec 2010 Posts: 11 Thanks: 0  Re: Resolution in Predicate logic
I have 4 sentences in CNF: Here are four sentences again: 1. (¬E(x) \/ V(x) \/ C(f(x))) /\ (¬E(x) \/ V(x) \/ S(x,f(x))) 2. P(a) /\ E(a) /\ (¬S(a,y) v P(y)) 3. ¬V(z) \/ ¬P(z) 4. C(b) /\ P(b) This is my knowledge base. Now I think I need to add the negation of my conclusion sentence (4) to KB, that is to add, 5. ¬(C(b) /\ P(b)) Then I have to resolve complement literals, and disprove KB /\ 5, in order to prove 4. Representing them again, we have: 1) ~E(x) v V(x) v C(f(x)) 2) ~E(x) v V(x) v S(x,f(x)) 3) ~S(a,y) v P(y) 4) ~V(z) v ~P(z) 5) ~C(b) v ~P(b) 6) P(a) 7) E(a) The thing is that they do not look like complements because they need unification and substitution. Any help with this? Thanks 
January 4th, 2011, 03:26 AM  #9 
Senior Member Joined: Nov 2010 From: Staten Island, NY Posts: 152 Thanks: 0  Re: Resolution in Predicate logic
I don't see why you need number 5. Here is the list of consequences with the reasons on the right: \neg V(a)" /> 6,4 7,8,1 7,8,2 10,3 9.11 12 
January 4th, 2011, 06:54 AM  #10 
Newbie Joined: Dec 2010 Posts: 11 Thanks: 0  Re: Resolution in Predicate logic
Thanks DrSteve, I need 5 because this is the way resolution works; to disprove the union of 5 with knowledge base in order to prove 4, the negation of 5. Thanks again anyway. That was helpful. 

Tags 
logic, predicate, resolution 
Thread Tools  
Display Modes  

Similar Threads  
Thread  Thread Starter  Forum  Replies  Last Post 
predicate logic  skaur  Applied Math  1  January 6th, 2014 06:51 PM 
Predicate Logic  mohitpd  Applied Math  0  October 26th, 2013 08:45 PM 
Predicate Logic  pavankumar.thati  Applied Math  0  April 16th, 2013 10:26 AM 
Predicate Logic translation. >_<  pinkcheese  Applied Math  0  November 22nd, 2010 09:40 PM 
Sets and Predicate logic  Zhai  Applied Math  7  February 22nd, 2010 07:32 PM 