- From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
- Date: Fri, 17 Dec 2004 16:38:18 -0500 (EST)
- To: sandro@w3.org
- Cc: www-rdf-logic@w3.org
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