Re: same-syntax extensions to RDF

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