Results 1 to 12 of 12

Math Help - Resolution in Predicate logic

  1. #1
    Newbie
    Joined
    Dec 2010
    Posts
    12

    Resolution in Predicate logic

    I need help with the following question:

    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.


    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.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    A Plied Mathematician
    Joined
    Jun 2010
    From
    CT, USA
    Posts
    6,318
    Thanks
    4
    Awards
    2
    1. For your FOL translation of 1, I would move a right parenthesis much farther to the right. That is, instead of

    ∀x (E(x) /\ V(x)) --> ∃y (C(y) /\ S(x,y)

    I would have

    ∀x ((E(x) /\ V(x)) --> ∃y (C(y) /\ S(x,y)).

    Otherwise, the scope of the x quantifier is curtailed prematurely: you need it in the S(x,y) predicate!

    2. You haven't quite captured the nuance that for some of those drug pushers entering the country, they were only searched by drug pushers. You have also curtailed the x quantifier too soon again. Try this on for size:

    ∃x ((P(x) /\ E(x)) /\ ∃y (S(x,y) --> P(y))).

    3. Careful with your parentheses. Look at this instead:

    ∀x (V(x) --> P(x))

    4. Again, careful with your parentheses. Try this instead:

    ∃x (C(x) /\ P(x)).

    You can get prenex normal form quite easily for all these statements, I think. Once you get prenex, it shouldn't be too hard to get CNF inside the quantifier parts. What do you get?
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Dec 2010
    Posts
    12
    Thanks Ackbeet for your help,

    The thing is that i am quite new and amateur in logic and not familiar with 'prenex'. anyway, I would try again to see what can i do with this. Thanks again.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    Newbie
    Joined
    Dec 2010
    Posts
    12
    Here are sentences in 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)

    Next I need to do resolution...
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Newbie
    Joined
    Dec 2010
    Posts
    12
    Here it is again,

    I have 4 sentences in 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)

    This is my knowledge base. Now I think I need to add the negation of 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. I am stuck. Any help? Thanks
    Follow Math Help Forum on Facebook and Google+

  6. #6
    A Plied Mathematician
    Joined
    Jun 2010
    From
    CT, USA
    Posts
    6,318
    Thanks
    4
    Awards
    2
    I haven't forgotten about you, but this post is rapidly reaching the end of my knowledge, which is why I've invited emakarov to take over this thread.

    Cheers.
    Follow Math Help Forum on Facebook and Google+

  7. #7
    Newbie
    Joined
    Dec 2010
    Posts
    12
    Thanks...
    Follow Math Help Forum on Facebook and Google+

  8. #8
    Member
    Joined
    May 2010
    Posts
    95
    Quote Originally Posted by agaton View Post

    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) P(a)
    6) E(a)


    (*) C(b) /\ P(b)
    Hey, it is a quite long procedure to obtain (1-6), so I'll assume your procedure is correct and start with (1-6), and show (*).

    By (1), (6), and the generalization theorem, we obtain

    (7) V(x) v C(f(x)).

    Similarly,
    (8) V(x) v S(x,f(x)).
    (9) ~V(z).

    By (7) and (9) with subst{z/x}, we have
    (10) C(f(x)).
    (11) S(x, f(x))
    From (10-11) by using existential instantiation, we have
    (12) C(b) /* b has not been used so far. */
    (13) S(x, b)
    From (3) by subst{y/b} and (13) by subst{x/a}, we have
    (14) P(b)

    From (12) and (14), we conclude (*) C(b) /\ P(b).
    Follow Math Help Forum on Facebook and Google+

  9. #9
    Newbie
    Joined
    Dec 2010
    Posts
    12
    Thanks TheArtofSymmetry
    Follow Math Help Forum on Facebook and Google+

  10. #10
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,530
    Thanks
    774
    I have just seen this thread, so I'll start from the beginning.

    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... Conclude by resolution that some of the officials were drug pushers.
    ∀x ((E(x) /\ V(x)) --> ∃y (C(y) /\ S(x,y))
    ∃x ((P(x) /\ E(x)) /\ ∃y (S(x,y) --> P(y)))
    ∀x (V(x) --> P(x))
    ∃x (C(x) /\ P(x))
    I agree except for the second premise, where ∃y (S(x,y) --> P(y)) should be replaced by ∀y (S(x,y) --> P(y)). I have to think a bit about how to motivate this, but meanwhile, I don't think the desired conclusion can be derived with ∃y. Indeed, let's call the pusher who entered the country a; then from the first premise (also using the third one) we have the custom official who searched a. Now we need to apply ∀y (S(x,y) --> P(y)) to this very official. If it said ∃y (S(x,y) --> P(y)), then it could refer to a completely unrelated official.

    When you translate the second premise into the Skolem normal form P(a) /\ E(a) /\ (S(a,y) v P(y)), you correctly consider that y is bound by a universal quantifier, so it is not replaced by a fresh constant.

    Incidentally, concerning the scope of quantifiers, I like the convention used by a famous logician Helmut Schwichtenberg in this article (footnote 1):
    Notice our slightly unusual formula notation: the scope of a quantifier followed by a dot extends as far as the surrounding parentheses allow. Otherwise we follow the standard convention that quantifiers bind stronger than /\, which binds stronger than ->.
    The second premise would then be expressed as ∃x. P(x) /\ E(x) /\ ∀y. S(x,y) --> P(y).

    have 4 sentences in 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)

    This is my knowledge base. Now I think I need to add the negation of conclusion sentence (4) to KB, that is to add,

    5. (C(b) /\ P(b))
    I agree except for the negation of the conclusion. One must first form the negation of the original conclusion that has to be proved and then convert it into a Skolem normal form, not the other way around. Negating ∃x. C(x) /\ P(x) produces a universal quantifier, so the result is ~C(x) \/ ~P(x) for a variable, not a constant, x.

    Concerning the derivation in post #8, ~E(x) v V(x) v C(f(x)) and E(a) do not imply V(x) v C(f(x)), only V(a) v C(f(a)), and, in any case, the derivation must use the resolution rule only (it is sound and complete). My derivation has 12 steps and follows the informal reasoning. First we prove ~V(a) (the pusher a is not a VIP) and use it to show C(f(a)) and S(a,f(a)) (the official f(a) searched a). Then we get P(f(a)) from the third conjunct of the second hypothesis and derive the empty disjunct from the negation of the conclusion and C(f(a)).
    Follow Math Help Forum on Facebook and Google+

  11. #11
    Member
    Joined
    May 2010
    Posts
    95
    Quote Originally Posted by emakarov View Post
    Concerning the derivation in post #8, ~E(x) v V(x) v C(f(x)) and E(a) do not imply V(x) v C(f(x)), only V(a) v C(f(a)), and, in any case, the derivation must use the resolution rule only (it is sound and complete). My derivation has 12 steps and follows the informal reasoning. First we prove ~V(a) (the pusher a is not a VIP) and use it to show C(f(a)) and S(a,f(a)) (the official f(a) searched a). Then we get P(f(a)) from the third conjunct of the second hypothesis and derive the empty disjunct from the negation of the conclusion and C(f(a)).
    Thank you.
    Last edited by TheArtofSymmetry; January 5th 2011 at 09:40 PM.
    Follow Math Help Forum on Facebook and Google+

  12. #12
    Newbie
    Joined
    Dec 2010
    Posts
    12
    Thanks emakarov, TheArtofSymmetry.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Predicate Logic
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: March 23rd 2011, 12:05 PM
  2. Predicate Logic #2
    Posted in the Discrete Math Forum
    Replies: 0
    Last Post: February 21st 2010, 08:34 PM
  3. Predicate Logic HELP.
    Posted in the Discrete Math Forum
    Replies: 7
    Last Post: February 16th 2010, 08:54 AM
  4. predicate logic
    Posted in the Discrete Math Forum
    Replies: 10
    Last Post: March 6th 2009, 06:04 AM
  5. predicate logic
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: March 6th 2009, 01:06 AM

Search Tags


/mathhelpforum @mathhelpforum