Hi guys Previously i sent a post in a wrong section..... I am a newbie in Artifical Intelligence and currently reading a book "Expert Systems: Principle and Programming", I am working a question but don't know rather the answer is right. The question is: Give a formal proof using predicate logic for the following syllogism: No software is guaranteed All programs are software ------------------------ No programs are guaranteed. I defined the terms first S(x) = x is a software G(x) = x is guaranteed P(x) = x is a program then Assumes V = universal quantifier E = existential quantifier ~Vx S(x) -> G(x) Vx P(x) -> S(x) ~Vx P(x) -> G(x) and at the end I will be using Resolution Refutation Tree to prove it.... and I have got the result is invalid. Do any genius able to solve it? The textbook got questions but no answers so it is very hard for me to do the questions because i can't distinguish the solution is right or wrong. Do anyone know anything website provide the answer for it.

The problem is actually a very simple FOL proof, but you have just not translated your statements correctly!

You stated that "No software is guaranteed" <-> ~(Vx)(Sx -> Gx).

Igoring the initial ~, you have (Vx)(Sx -> Gx), which means "All software is guaranteed". So with the ~, you have "Not all software is guaranteed", which is different than the statement "No software is guaranteed". Here is another way of looking at it which is more mechanical where you're less likely to fall for this play on words:

Your wff can be translated roughly as "Some software is not guaranteed". To see this more clearly, use ~(Vx)(Px) <-> (Ex)~(Px), so we obtain ~(Vx)(Sx -> Gx) <-> (Ex)~(Sx -> Gx) <-> (Ex)~(~Sx v Gx) <-> (Ex)(Sx ^ ~Gx). This much more clearly translates to "There exists software which is not guaranteed", implying that some software could be guaranteed. (Using the same line of logic, your conclusion translation is also incorrect.)

I won't spoil the fun any further, but let us know if you need any more hints :-)


EDIT: In case you're curious, you're correct that your two axioms are not consistent with your conclusion! (As I'm sure you know, given Sx and Px -> Sx, no conclusion can be made about Px!)

[Edited by - mnansgar on May 3, 2006 9:16:18 AM]

Thanks for the precious reply..

So No Software is guaranteed = All software is not guaranteed.

I think I have got the answer right now, the conclusion seems to be correct, once the resolution tree has drawn the solution is towords the nil.

[Edited by - kbundy on May 3, 2006 5:02:10 PM]