Predicate logic ?

[jutah]

Sry this isn't a real programming Q, but Iam stuck and figured I might get some help here.

Here is the problem
Given:
All people who are not poor and are smart are happy. Those people who read are not stupid. Jill can read and is wealthy. John is poor and stupid. Happy people live exciting lives.

Use resolution to prove that there is someone with an exciting life. Who is it?

I have an idea of how to solve the problem. I know I have to put the english into pred logic convert that to Skolem normal form and then negate the conclusion and prove by contradction. The problem is Iam not sure if Iam converting the english to pred. logic right. Could I see how someone else would convert the previous enlish sentences into logic?

Thanks
Jutah :)

[scanez]

Let A = person who is not poor, B = smart person, C = happy person, D = person who can read, and E = person with exciting life. Then from the resulution we know that, A and B => C (A and B implies C), D => B, and C => E. Now for the people: Jill = D and A, John = not A and not B. But D => B, so Jill is also B and A.

Now can you tell who the person with the exciting person is?
SC

[ 31 October 2001: Message edited by: scanez ]

[jutah]

It looks like Jill. The way you organized the problem made it easier to understand, but I need to wright out the Pred. logic for ex. ForAll x [people(x) AND ~poor(x) AND smart(x)] => happy(x). Iam not sure if that is right though.

Thanks
Jutah

[knavely]

ok this is how i was taught
but you dont need to use the quantifiers i guess.
I just did because you said it was predicat logic.

Given:


1 (x)[( ~Px & Sx ) -> Hx]
2 (x)[Rx -> Sx]
3 (x)[Hx -> Ex]
4 Rj & ~Pj

universal instanciation we get

5 (~Pj & Sj) -> Hj
6 Rj -> Sj
7 Hj -> Ej
8 Rj line 4 Simp
9 ~Pj 4 simp
10 Sj 8,6 Modus Ponens
11 Sj & ~Pj 9,10 Conjunction
12 Hj 11,5 Modus Ponens
13 Ej 12,7 Modus Ponens

theres your person with the exiting life
14 Exists(x)[ Ex] 13 by Existential Generalization

[knavely]

ForAll x [people(x) AND ~poor(x) AND smart(x)] => happy(x).

i would do this:

x = people, so you dont need people(x)

(x)[( ~Poor(x) & Smart(x) ) -> Happy(x)]