# Thread: Resolution in Predicate logic

1. ## 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...

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))).

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

∃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?

3. 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.

4. 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...

5. 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

6. 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.

7. Thanks...

8. Originally Posted by agaton

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).

9. Thanks TheArtofSymmetry

10. 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)).

11. Originally Posted by emakarov
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.

12. Thanks emakarov, TheArtofSymmetry.