Re: same-syntax extensions to RDF

From: Sandro Hawke <sandro@w3.org>
Subject: Re: same-syntax extensions to RDF 
Date: Fri, 17 Dec 2004 15:59:10 -0500

[...]

> > > > Yes indeed.  The first seven triples may be entailed by the empty KB, if
> > > > you get the comprehension principles right, but somehow you need to get the
> > > > connection between.
> > > > 
> > > >     <a> <r> <b> .
> > > > 
> > > > and the truth of the encoding of the sentence R(a,b).   Otherwise how can
> > > > you say that you have captured FOL?
> > > 
> > > By design, Usable only goes one way.  So there's a connection, but not
> > > an if-and-only-if connection.   
> > 
> > But if there is no if-and-only-if then you really don't have logic.
> 
> As with "capturing" FOL, I'm not sure what that means.   I want to
> stuff FOL formulas down an RDF pipe and have them come out the other
> end in good working order, as in this test case:
> 
> > > I'm not quite sure what it would mean to "capture" FOL, so I'll be
> > > more specific. 
> > > 
> > > I want people to able to publish FOL assertions in RDF on the web so
> > > others can aggregate them (using RDF harvester/aggregators) and draw
> > > the normal FOL conclusions.   
> > > 
> > > For instance
> > >    e:yeshayah fam:brother e:sandro.
> > > from one source,
> > >    e:yeshayah fam:daughter e:eliana.
> > > from another source, and suitable definitions expressed at the fam:
> > > namespace in LX triples should allow one to conclude
> > >    e:eliana fam:uncle e:sandro.
> > 
> > Yes sure, but what happens if I assert (using your machinery)
> >     ( <a> <r> <b> . ) & ( <c> <r> <d> . )
> > and some one else asks whether 
> >     ( <c> <r> <d> . ) & ( <a> <r> <b> . )
> > follows from this?  Or, and more difficult to get right, what happens 
> > if I assert (using your machinery)
> >    A x ( <a> <r> x . )
> > and some one else asks whether 
> >     <a> <r> <b> .
> > follows?
> > 
> > If your formal machinery doesn't support this then it really hasn't
> > captured logic at all.
> 
> It does support that.   Those example are fine.

But I don't see how this can work, even disregarding any details.

If all you have is Usable, and there is no way to infer Usable, then how
can the truth of 
   ( <c> <r> <d> . ) & ( <a> <r> <b> . )
be derived from that of
   ( <a> <r> <b> . ) & ( <c> <r> <d> . )


> Well, I guess it really depends on the API and whether "the system" is
> trying to be an entailment checker, a query answering service, a
> consistency checker, an inconsistency checker, etc, ....   but I don't
> see any particular problems with the query-answering use case.   

Well, entailment is, to me, what FOL is all about.  If you don't have
entailment, how can you get any of the rest?  



> > > > > Here I think you're asking whether
> > > > >    for some _:SA_left, _:SA_lefts, _:SA_leftp, _:SA_lefto
> > > > >    _:SA_left lx:subjectTerm _:SA_lefts.
> > > > >    _:SA_left lx:predicateTerm _:SA_leftp.
> > > > >    _:SA_left lx:objectTerm _:SA_lefto.
> > > > >    _:SA_lefts lx:denotation <a>.
> > > > >    _:SA_leftp lx:denotation <r>.
> > > > >    _:SA_lefto lx:denotation <b>.
> > > > >    _:SA_left rdf:type lx:Usable.
> > > > > and
> > > > >    for some _:SA_right, _:SA_rights, _:SA_rightp, _:SA_righto
> > > > >    _:SA_right lx:subjectTerm _:SA_rights.
> > > > >    _:SA_right lx:predicateTerm _:SA_rightp.
> > > > >    _:SA_right lx:objectTerm _:SA_righto.
> > > > >    _:SA_rights lx:denotation <c>.
> > > > >    _:SA_rightp lx:denotation <r>.
> > > > >    _:SA_righto lx:denotation <d>.
> > > > >    _:SA_right rdf:type lx:Usable.
> > > > > together entail
> > > > >    for some _:x, _:left, _:lefts,  _:leftp,  _:lefto
> > > > >                  _:right , _:rights,  _:rightp,  _:righto
> > > > >    _:x rdf:type lx:Conjunction.
> > > ...
> > > > >    _:x rdf:type lx:Usable.
> > > > > 
> > > > > which I believe I can show.  
> > > >
> > > > Well, yes, I would like to see how this works.  I didn't see anything tha
> > t
> > > > gives me reason to believe that it does follow, however.  In particular I
> > > > don't see anything in the rationale for Usable that could lead to the
> > > > possiblity of inferring that Usable was the type of any resource.
> > > 
> > > You're right, I was overly hasty in thinking that entailment held.  We
> > > don't need it for my use cases, and to provide for it gets problematic
> 
> > 
> > See above.
> > 
> > The ability to derive consequences is the heart of a logic.  If you can't
> > get FOL entailment from your machinery you haven't done FOL.
> 
> Sure, but the entailments are not in the reified form, they are in the
> ordinary de-refied form.   
> 
> In KIF-like syntax:
> 
>    (Usable (r a b))
> entails
>    (r a b)
> 
> and
>    (Usable (and (r a b) (r c d)))
> entails
>    (and (r a b) (r c d)))
> which of course entails
>    (r a b)
> and
>    (r c d)

But how can you get 
     (r a b)
entails
    (Usable (r a b))
or, more importantly,
     (r a b)
entails
    (Usable ( or (r a b) (r c d) ) )
or
     (r a b)
entails
    (Usable (exists x (r a x)))

If you don't get these, how can you claim to be doing FOL?

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

It looks as if you only want 1/n'th of FOL.  OK, if that is what you want,
then you might be able to get it.  However, I thought that the goal was to
get all 1/1'th of FOL.  Also, I'm not sure which 1/n'th of FOL you want, so
I can't figure out whether you are on a path to success.

>     -- sandro

peter

Received on Friday, 17 December 2004 21:38:26 UTC