Pro found, but missing Log

From: Ben (serpent11_at_hotmail.com)
Date: 11/30/03 

Date: Sun, 30 Nov 2003 05:58:56 GMT

Hi:

This is a homework question, so don't give me any straight-up answers,
please. I will note that I received help from this newsgroup on the
assignment.

I essentially have to show whether some attribute of a first-order
logic statement is valid, satisfiable or unsatisfiable after
unification and resolution (it turns out that this one is
satisfiable). The statement follows from a given paragraph. I tried
converting the paragraph to a ProLog knowledge base in several ways,
first assuming that I could be very cheap about it and then being more
specific, but it still gives an existence error every time I try to
run it. Some of my attempts follow:

immortal(unicorn) :- mythical(unicorn).
(not(immortal(unicorn)) , mammal(unicorn)) :- not(mythical(unicorn)).
horned(unicorn) :- (immortal(unicorn) | mammal(unicorn)).
magical(unicorn) :- horned(unicorn).

The most noteworthy thing about this knowledge base is that there are
no actual attributes given. Everything is conditional on the unicorn
having some other attribute.

I later tried converting everything to the if-then statements in a
form like this just to see if I could make it work:

blah(unicorn) := [not] foo(unicorn).

Note that all of these attempts compiled into bytecode without errors.

And still when I entered the ultimate goal, to determine whether these
rules entail mythical(unicorn), I get the existence error.

My biggest question is this, a question that I can't get a straight
answer for anywhere: I know that a comma is a logical and in ProLog,
but what about or and not? No references or examples seem to contain
any information on that, and I've been through numerous tutorials and
manuals on the web. It would also be helpful to know what answer I
should expect to get from ProLog if mythical(unicorn). if the solution
is valid, unsatisfiable, or satisfiable (Yes and No don't seem to be
sufficient to cover 3. Should I expect something like this?)
                     mythical(unicorn) not mythical(unicorn)
Valid Yes No
Unsatisfiable No Yes
Satisfiable Yes Yes

Finally, just how far off was my original code above from something
that might have worked? Can I even do something cheap like (Not A |
B) := Not C?

Thanks for your time and help,
~Ben

http://www.snakebyte.biz