Re: semantics status of RDF(S)

> > >When using resolution one cannot have such p->false rules.
> >
> > Incorrect. In fact, resolution REQUIRES the use of such clauses.
>
>Of course it requires the use of such clauses, but only ONE
>such clause, namely for the goal to be proved

No, that is not correct. Resolution can be applied to any clauses. 
Maybe some Prolog interpreters require there to be at most one 
negated goal clause, but even Horn clause form doesnt state that 
there must be only *one* negated clause.

> > >So one cannot (as such) deny the fact that p is true.
> >
> > Yes, one can. If one could not deny it, resolution could never find a
> > contradiction.
>
>I could see the use of negation in the premises of rules
>but not as
>  false :- p
>rules in a prolog program for instance

Well, I agree that would be very odd Prolog (though I think it is 
technically not incorrect), but Prolog and resolution are not the 
same thing.

>maybe I'm missing something in my knoledge of resolution ...
>
> > >There is however an easier problem (maybe).
> > >On the proof level (where proof expressions live)
> > >we can discover that p has a no-proof-found value.
> > >Of course that is not the denial of p but that
> > >is not a problem for a proof expressions's life!
> > >All it has to express is evidence that can be
> > >syntactically checked to give semantic validity
> > >(and such expressions can contain p->false
> > >parts coming from negated premisses).
> >
> > I have no idea what you are talking about in the above paragraph. Can
> > you rephrase it? In particular, what is the 'proof level' ?
>
>The proof level is what TimBL has drawn so nicely in
>http://www.w3.org/2001/Talks/0228-tbl/slide5-0.html

You really should not confuse a picture with a definition. I repeat, 
what *is* the 'proof level'?

Pat Hayes

---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Monday, 9 April 2001 14:23:59 UTC