Re: semantics status of RDF(S)

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

I see that our phrasing is indeed ussuming a lot of
implicit things ...
The proof level is what TimBL has drawn so nicely in
http://www.w3.org/2001/Talks/0228-tbl/slide5-0.html
We also assume a proof expression to be a propositional
logic formula. Of course this is not yet a proof language!
Such a proof can be the result of e.g. predicate logic
inferences (using e.g. binary predicate reflexive resolution,
but of course there are many, many proof engine technologies).
I want to refer here to the stuff that we have exemplified
at http://www.agfa.com/w3c/euler/ (just to fix the idea).
In there the so called proofs are nested material
implications. If those proofs are posed as a new lemma
one obtains a so called checked proof (which is actually
a fixpoint when also posed as a lemma).
A checked proof is somehow giving the syntactic validity
  axioms |- lemma
and as we know from symbolic logic
  syntactic validity |- implies semantic validity |=
  (but not necessarily the other way around according to
  an interpretation of Goedel's incompleteness theorem).
Proof checking is indeed a straightforward thing (certainly
compared to proof generation) and if no proof could be
generated, the proof check of that will be even simpler ...

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

Received on Monday, 9 April 2001 09:09:05 UTC