Resolution in predicate logic

[Agaton]

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.






Thanks in advance.

 

[honestrosewater]

So I just now read about resolution and Skolemization, but it sounds mostly straightforward.

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

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

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

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

These are all fine.

∀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

You forgot to switch to disjunction here.

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

Do you have variables and constants in your language? Do you have any examples of what count as CNF forms? I'm wondering what your literals look like. If you have variables, the universally-quantified variables just become free variables. The existentially-quantified variables become Skolem functions, i.e., functions of the universally-quantified variables whose scope there are in. Only the existentially-quantified variables not within the scope of any universal quantifier can become constants (or 0-ary functions). So (4) can become C(a) & P(a) but the y in (1) would need to be f(x) because it's in the scope of the universal quantifier of x.(Are you writing an automated theorem-prover?)

 

[Agaton]

Dear

Thank you very much for your comment.
I am quite new in logic. what I see is that the first sentence, after removing implication, is in DNF and i need to convert it to CNF, then skolamization and finally resolution. Is this correct? I just do not know how to convert it from DNF to CNF!

 

[honestrosewater]

Well, it makes more sense to me to remove the quantifiers before converting to CNF.

1. ∀x((E(x) & ~V(x)) -> ∃y(C(y) & S(x,y)))
1. (E(x) & ~V(x)) -> (C(f(x)) & S(x,f(x)))
1. ~(E(x) & ~V(x)) v (C(f(x)) & S(x,f(x)))
1. (~E(x) v V(x)) v (C(f(x)) & S(x,f(x)))
Use distribution to swap around conjunctions and disjunctions (P v (Q & R) <=> (P v Q) & (P v R)).
1. ((~E(x) v V(x)) v C(f(x))) & ((~E(x) v V(x)) v S(x,f(x)))
Drop unnecessary parentheses.
1. (~E(x) v V(x) v C(f(x))) & (~E(x) v V(x) v S(x,f(x)))

Are you allowed to have literals of this form?

 

[Agaton]

Thank you,

I think I can just use constants for quantifier elimination. I do not know any thing about literals! By the way, I am not writting anything, just trying to work on FOL.

 

[Agaton]

OK,

This is the sentences 1 & 4 as you represented:

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


1. ∀x ¬ (E(x) /\ ¬V(x)) \/ ∃y (C(y) /\ S(x,y)). //Implication elimination

1. ∀x (¬ E(x) \/ V(x)) \/ ∃y (C(y) /\ S(x,y)) //De Morgan

1. (¬ E(x) \/ V(x)) \/ (C(f(x)) /\ S(x,f(x)))

1. ((¬ E(x) \/ V(x)) \/ C(f(x))) /\ ((¬E (x) \/ V(x)) \/ S(x,f(x))) //Using distribution

1. (¬E(x) \/ V(x) \/ C(f(x))) /\ (¬E(x) \/ V(x) \/ S(x,f(x))) // Dropping unnecessary parentheses



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

4. C(a) /\ P(a)


I also changed sentence 3 from ∀x V(x) ---> ¬P(x) to a new form ∀x ¬(V(x) /\ P(x)). This allows me to apply De Morgan:
3. ∀x ¬(V(x) /\ P(x))

3. ∀x (¬V (x) \/ ¬P(x)) //De Morgan

I think this now need a skolem function, but i am not sure how to do that again. I have the same problem with sentence 2 as well:

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

Thank you.

 

[honestrosewater]

A literal is an atomic formula or the negation of an atomic formula. In propositional logic, the atomic formulas are just propositional variables. But here, the atomic formulas are predications. So E(x), ~E(x), P(x,y), and ~P(a) are all literals.

Do you understand how ∃y[P(y)] can become P(a) for some constant a? Do you see a problem with turning ∀x∃y[P(y,x)] into P(a,x)? Imagine that P(y,x) means y is the mother of x. Then ∀x∃y[P(y,x)] means everyone has a mother. But P(a,x) loses this relationship and makes a the same for every x. So you need to hold onto the relationship between y and x by making y a function of x: P(f(x),x). Now the function can do what you need: map every x to their mother. That's Skolemization.

Does it make sense yet?

 

[Agaton]

Thank you very much for your explanation. It was very clear in comparison to books. when you say P(a,x) makes a the same for every x, You mean it hasn't got the generality we have in ∀x∃y[P(y,x)]? Am I correct?

Thank you.

 

[Agaton]

Following your comments, I have the above 4 sentences in CNF, as it follows:

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


1. ∀x ¬ (E(x) /\ ¬V(x)) \/ ∃y (C(y) /\ S(x,y)). //Implication elimination

1. ∀x (¬ E(x) \/ V(x)) \/ ∃y (C(y) /\ S(x,y)) //De Morgan

1. (¬ E(x) \/ V(x)) \/ (C(f(x)) /\ S(x,f(x)))

1. ((¬ E(x) \/ V(x)) \/ C(f(x))) /\ ((¬E (x) \/ V(x)) \/ S(x,f(x))) //Using distribution

1. (¬E(x) \/ V(x) \/ C(f(x))) /\ (¬E(x) \/ V(x) \/ S(x,f(x))) // Dropping unnecessary parentheses



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

2. [P(a) /\ E(a) /\ S(a,f(m))]



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

3. ¬V(x) \/ P(x) // Universal quantifier elimination and Implication elimination


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

4. C(a) /\ P(a)



Are they in CNF now?

Thanks,

 

[honestrosewater]

You mean it hasn't got the generality we have in ∀x∃y[P(y,x)]? Am I correct?

Sure. If you didn't distinguish between an existential quantifier being inside vs. outside the scope of a universal quantifier, then ∀x∃y[P(y,x)] and ∃y∀x[P(y,x)] would both get turned into the same formula, and the latter says everyone has the same mother.

Following your comments, I have the above 4 sentences in CNF, as it follows:

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


1. ∀x ¬ (E(x) /\ ¬V(x)) \/ ∃y (C(y) /\ S(x,y)). //Implication elimination

1. ∀x (¬ E(x) \/ V(x)) \/ ∃y (C(y) /\ S(x,y)) //De Morgan

1. (¬ E(x) \/ V(x)) \/ (C(f(x)) /\ S(x,f(x)))

1. ((¬ E(x) \/ V(x)) \/ C(f(x))) /\ ((¬E (x) \/ V(x)) \/ S(x,f(x))) //Using distribution

1. (¬E(x) \/ V(x) \/ C(f(x))) /\ (¬E(x) \/ V(x) \/ S(x,f(x))) // Dropping unnecessary parentheses

This looks fine.

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

2. [P(a) /\ E(a) /\ S(a,f(m))]

Well, the change isn't right, but I just realized that the original interpretation should be slightly different.

2. Some of the drug pushers entered this country and they were only searched by drug pushers.​

You need universal quantification for the only part. If only drug pushers searched them, then for all x, if x searched them, then x was a drug pusher:

∃x[P(x) /\ E(x) /\ ∀y[S(x,y) -> P(y)]]

But you might find it helpful to bring the quantifiers out to the front for prenex form (keeping them in the right order).

∃x∀y[P(x) /\ E(x) /\ (S(x,y) -> P(y))]

Since ∃x comes before ∀y, it's not in its scope, so you can just replace x with a (fresh!) constant and drop ∀y.

P(a) /\ E(a) /\ (S(a,y) -> P(y))
P(a) /\ E(a) /\ (~S(a,y) v P(y))

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

3. ¬V(x) \/ P(x) // Universal quantifier elimination and Implication elimination

Good except that you need a fresh variable. You have used x in (1) already.

¬V(z) \/ P(z)

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

4. C(a) /\ P(a)

Fresh constant again.

C(b) /\ P(b)

Do you see why you need fresh constants and variables?

How do you do with resolution?

 

[Agaton]

Thanks again,

About the constants, I was thinking whether they have to be same or not, but was not sure what I really mean by that! Thanks for reminding the point. I guess constants cannot be same, because they stand for different 'things'. Is that right?Now Resolution:

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

Is this correct? The above sentences does not look like complemets to each other!

 

[honestrosewater]

I guess constants cannot be same, because they stand for different 'things'. Is that right?

Yes, sort of. They're actually arbitrary constants, so they could in a sense stand for the same thing. But that brings me to the limits of what I know about the system you're using, so I can't say more about what they refer to or how. But it's enough to think of them standing for different things in the other direction: they stand for the different bindings that they instantiated. Say that E(x) means x is even and P(x) means x is a prime greater than 5. Consider

1) ∃x[E(x) & P(x)]
2) ∃x∃y[E(x) & P(y)]

If the variables are taken to range over integers, then (1) is false and (2) is true. There do exists even numbers and prime numbers greater than 5, but there are no numbers that are both. Using fresh constants for instantiation preserves this:

1) ∃x[E(x) & P(x)] ==> E(a) & P(a)
2) ∃x∃y[E(x) & P(y)] ==> E(a) & P(b)

If you failed to use fresh constants, (1) and (2) would become the same after instantiation:

1) ∃x[E(x) & P(x)] ==> E(a) & P(a)
2) ∃x∃y[E(x) & P(y)] ==> E(a) & P(a)

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)

5. ¬(C(b) /\ P(b))

Then I have to resolve complement literals, and disprove KB /\ 5, in order to prove 4.

Is this correct? The above sentences does not look like complemets to each other!

Right, you want to try to derive the empty clause. Don't forget to convert (5) to CNF. What are your resolution and unification rules? I am not sure how to unify f(x) with anything else. How far can you get with this?

 

[honestrosewater]

It might help to clean things up some, like so:

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)

You have options there. What if you resolve (4) and (5)?

 

[Agaton]

honestrosewater, thank again.

I think I had a mistake when I removed implication in 3

3. ∀x V(x) ---> ¬P(x)
3. ¬V(x) \/ P(x)

The correct sentence after implication elimination should be this:

3. ¬V(z) \/ ¬P(z)

Am I right?

 

[honestrosewater]

Oh, yeah, I didn't even notice that. So you can resolve (3) with (4) or (5).

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)

 

[Agaton]

Thanks,

I just reviewed unification and substitution concept in resolution. Do I need to unify or substitute and variable? or do i need just to translate them to natural language and then resolve?!

For example, Do I need to translate sentences 4 and 5 as:

4. That is not the case that z is a VIP or drug pusher.

5. That is not the case that b is custom official or drug pusher.

Then, from 4 & 5, I get ~V(z) v ~C(b)!

?

 

[honestrosewater]

Well, I don't know what your rules say, but I don't see why translation would be necessary or helpful. You can't resolve (4) and (5) anymore since P(z) was corrected to ~P(z). You need to find complementary literals. So (3) with (4) or (3) with (5) or lots of others. Do you know how to unify functions with variables and constants? Since V and S are together in (2), I would resolve (3) with (4), which I imagine would look like

3) ~S(a,y) v P(y)
4) ~V(z) v ~P(z)
/unification
3) ~S(a,y) v P(y)
4) ~V(y) v ~P(y)
/resolution
8) ~S(a,y) v ~V(y)

Now what?

 

[Agaton]

I haven't got any special rules, just trying to do this in FOL.

I also do not know how to unify with constants. I saw a few examples in books, but this is much more complicated that those. Can you finish it please?
Thanks

 

[honestrosewater]

Just match up the complements. You have several. I suppose it makes sense for a function to become a variable or a constant in unification, and if unifying two functions, the higher arity one becomes the lower arity (which is a generalization of the first rule).

1) ~E(x) v V(x) v C(f(x))
2) ~E(x) v V(x) v S(x,f(x))
5) ~C(b) v ~P(b)
6) P(a)
7) E(a)
8) ~S(a,y) v ~V(y)

Which two would you resolve next (to get to the empty clause)?

 

[Agaton]

I am not sure whether I understand it...even the one you already resolved, that is 3&4...

 

[honestrosewater]

Okay, what part do you understand? Do you know any other formal proof systems? Can you show by any means that this formula is always true?

((A v B) & (~A v C)) -> (B v C)

 

[Agaton]

emmm,
not sure but I think I need to determine the truth value of each sentence first, and then the truth value of the conditional, by using rules and equivalences. right?

 

[honestrosewater]

Sure, you can do it many ways. If you don't have a formal system, you can think about it this way.

0) ((A v B) & (~A v C)) -> (B v C)

(0) is an implication formula (i.e., its topmost operator is implication). An implication is only false when the antecedent is true and the consequent is false, yes? So assign values to the atomic formulas in such a way that the antecedent is true. Then check the truth value of the consequent. If it is true, then the implication can never be false. Yeah?

The consequent is a disjunction, which is true whenever at least one of its disjuncts is true. So as long as our assignments force at least one of the disjuncts to be true, we're good.

Let A be true. Then ~A is false, so for the antecedent to be true, C must be true. Let A be false. Then B must be true. So (0) is always true.

Resolution just puts (0) to use as a derivation rule. It says that if you have a set of formulas, and two of them are of the forms A v B and ~A v C, then since (0) is always true, your set implies B v C, and so you can add B v C to your set without changing the models that will satisfy it. Make sense?

You have a set of formulas:

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)

You want to pick some atom to take the role of A in (0). I'm going to choose the P/1 in (3) and (4). You unify the two versions of your A: P(y), ~P(z). Since y and z are both variables, they just become the same variable, which I'm going to call y. So change all of the zs in (3) and (4) to ys:

3) ~S(a,y) v P(y)
4) ~V(y) v ~P(y)

Now you can combine them and use your resolution rule. You have

(~S(a,y) v P(y)) & (~V(y) v ~P(y))

and you know

(~S(a,y) v P(y)) & (~V(y) v ~P(y)) -> (~S(a,y) v ~V(y))

must be true, so you can add

8) (~S(a,y) v ~V(y))

You can keep (3) and (4) around, but since you already used them, it's easier for you to cross them off.

Now you keep going. Pick another A. Keep in mind that since you are doing a proof by contradiction, you are trying to end up with (A & ~A), which you can think of (in a slightly abusive way) as a special case of (0) where there is no B or C, so you end up with the empty clause.

 

[Agaton]

Very expressive and helpful, I mean all your comments on this topic. Thank you. I need to work on FOL and resolution more, and this was a very good start point.