W3C home > Mailing lists > Public > www-rdf-logic@w3.org > April 2001

Re: semantics status of RDF(S)

From: <jos.deroo.jd@belgium.agfa.com>
Date: Mon, 9 Apr 2001 15:08:55 +0100
To: phayes@ai.uwf.edu
Cc: www-rdf-logic@w3.org, aswartz@swartzfam.com
Message-Id: <OF69AD7DA0.2A4AC3A6-ON41256A29.003D7DCB@bayer-ag.com>


> >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 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:52:38 GMT