- From: Sandro Hawke <sandro@w3.org>
- Date: Sat, 18 Dec 2004 15:02:43 -0500
- To: Tanel Tammet <tammet@staff.ttu.ee>
- Cc: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, www-rdf-logic@w3.org
> >The goal, again, is for someone to be able to express the definition > >of fam:uncle in RDF in a way which supports the obvious inferences and > >causes no serious problems. If it's not clear yet how this design > >does that, what would help clarify it? > > > > > > > I do not have much to add to this discussion. Rather, I'd propose > another angle to look at the possibility to encode FOL in RDF. > > As far as I understand, RDF does not have universally quantified > variables and is obviously decidable. RDFS has universally > quantified variables in some specific formulas (taxonomy > implications), but is still decidable. > > FOL, on the other hand, is undecidable. Hence you cannot encode FOL > in RDF(S), using RDF(S) semantics and nothing more. Agreed. > On the other hand, you can write FOL sentences as bitstrings, > hence you can obviously write them as RDF sentences too. I think it's misleading to say that writing FOL inside bitstrings which occur in RDF is the same as writing them "as RDF". I'll show this more below. > However, such RDF usage would have no logical meaning > (i.e. you need an external mechanism for derivations) and > would not be especially interesting, Right, but adding "external mechanism" is fine, right? That's what OWL does, and what RDFS does to RDF: it introduces some vocabulary terms, and RDF sentences which use those terms have meaning to agents following the relevant specs. (Peter put it more precisely in his reply to you.) > Since this is pretty obvious, I was a bit puzzled by the issue > you were discussing. Could you clarify a bit: what was the > main idea of the question Sandro posed? I'll rephase my first message [1] using the bitstring approach. To have my fam:uncle example work, the FOL sentence which is carried needs to be somewhat integrated with RDF, right? It can't just say all Brother Child ( (exists Parent ( brother(Parent, Brother) & child(Parent, Child) ) <-> uncle(Child, Brother) ). because those predicates ("brother", "child", and "uncle") are not tied to the RDF world; that uncle predicate isn't connected to the URI abbreviated fam:uncle, etc. Instead we need to say something like: all Brother Child ( (exists Parent ( fam:brother(Parent, Brother) & fam:child(Parent, Child) ) <-> fam:uncle(Child, Brother) ). or, to use a form I prefer because it avoids the "HiLog" issue: all Brother Child ( (exists Parent ( rdf(Parent, fam:brother, Brother) & rdf(Parent, fam:child, Child) ) <-> rdf(Child, fam:uncle, Brother) ). Now, we can throw this in a plain (string) literal, if we want, but how do we say which such strings in a chunk as RDF are to be understoood as asserted FOL in this otter-ish syntax? Exactly what RDF would you use to convey the above rule? Now we're back at part 3 of my original e-mail. The simplistic approach is to say _:x lx:otterText " all Brother Child ((exists Parent (rdf(Parent, fam:brother, Brother) & rdf(Parent, fam:child, Child)) <-> rdf(Child, fam:uncle, Brother)). ". _:x rdf:type lx:TrueSentence. but the fact that we can easily constuct a Liar Paradox out of that suggests it's not a very good formalism. Do you see a simpler/better one which handles my fam:uncle test case but doesn't have problems with the Liar? Alternatively, maybe the ability to write a paradox isn't a real problem, but I don't want to argue that. Do you see the challenge now? My solution is to use lx:Usable instead of lx:TrueSentence, but that makes some aspects more confusing; that's what I'm trying to work out in this discussion. -- sandro [1] http://lists.w3.org/Archives/Public/www-rdf-logic/2004Dec/0008
Received on Saturday, 18 December 2004 19:59:46 UTC