My Math Forum Resolution in Predicate logic

 Applied Math Applied Math Forum

 December 31st, 2010, 04: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, 05: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) $\forall x ((E(x)\wedge\neg V(x))\rightarrow \exists y(C(y)\wedge S(x,y)))$ (2) $\exists x(P(x)\wedge E(x)\wedge \forall y(S(x,y)\rightarrow P(y)))$ (3) $\forall x (V(x)\rightarrow \neg P(x))$ $\therefore \exist x(C(x)\wedge P(x))$ 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, 01: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, 08: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 $\forall x \phi (x) \rightarrow \phi (x)$ is a logical axiom, so you can drop the initial $\forall x$ $(E(x)\wedge \neg V(x))\rightarrow \exists y ((C(y)\wedge S(x,y))$ $\neg (E(x)\wedge \neg V(x))\vee \exists y ((C(y)\wedge S(x,y))$ $(\neg E(x)\vee V(x))\vee \exists y ((C(y)\wedge S(x,y))$ $(\neg E(x)\vee V(x))\vee (C(a)\wedge S(x,a))$ $\neg E(x)\vee (V(x)\vee (C(a)\wedge S(x,a)))$ $(\neg E(x)\vee V(x)\vee C(a))\wedge (\neg E(x)\vee V(x) \vee S(x,a))$ Note that your second sentence is wrong (compare with mine in my first post). Hope this helps.
 January 1st, 2011, 02: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, 02: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, 04:38 AM #7 Newbie   Joined: Dec 2010 Posts: 5 Thanks: 0 Re: Resolution in Predicate logic DrSteve, thanks again.
 January 3rd, 2011, 02: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, 02: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 $9) C(f(a))$ 7,8,1 $10) S(a,f(a))$ 7,8,2 $11) P(f(a))$ 10,3 $12) C(f(a)) \wedge P(f(a))$ 9.11 $13) \exists x (C(x) \wedge P(x))$ 12
 January 4th, 2011, 05: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 Linear Mode

 Similar Threads Thread Thread Starter Forum Replies Last Post skaur Applied Math 1 January 6th, 2014 05:51 PM mohitpd Applied Math 0 October 26th, 2013 07:45 PM pavankumar.thati Applied Math 0 April 16th, 2013 09:26 AM pinkcheese Applied Math 0 November 22nd, 2010 08:40 PM Zhai Applied Math 7 February 22nd, 2010 06:32 PM

 Contact - Home - Forums - Cryptocurrency Forum - Top