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.

I had the resolution-as-implemented-by-prolog in mind and I
apparently have to refresh my understanding of the original
resolution algorithm of Robinson.

[...]

> > > >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'?

For the moment I would say (but I'm sure others can do it much better)
that proof-level is *the level where one deals with proofs*
(level in the context of information system architecture)

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Monday, 9 April 2001 18:32:26 UTC