- From: Sandro Hawke <sandro@w3.org>
- Date: Tue, 30 Apr 2002 07:06:43 -0400
- To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
- cc: phayes@ai.uwf.edu, www-rdf-logic@w3.org
** OOPS! Previous draft of this e-mail sent mid-edit! Please ignore it! ** Peter F. Patel-Schneider writes: > [...] > Sandro Hawke writes: > > Perhaps I'm misreading it; if someone can present a > > paradox using only log:forSome, log:forAll, and log:implies, then I > > think I (and I'll venture TimBL and others) will be very interested. > > [Hrm, I guess you'll have trouble until an n3->n-triples conversion is > > written down. It's in public e-mail between me and Tim; I'll dig it > > up if anyone seriously wants to try. The idea is to use > > log:Conjunction and daml:List to assemble an n3 Formula.] > > [...] > > You have to be more precise here. If *all* I can use is > log:forSome, log:forAll, and log:implies then I can't even make any > statement (because I don't have the . to finish the statement). I'm sorry for getting you interested and not giving you proper information. I really didn't expect anyone to approach that part of my message so suddenly. Silly me. I see several different styles of Horn logics for RDF. I think the kind I'm most comfortable with is typified by this example of mine [1], where every logical expression is reified, but more of the community seems comfortable with n3/cwm where many expressions (like "<x> implies <y>.") occur directly as triples. Let's stick to the more popular form for now. I'm going to try to restrict their imprecises semantics for quantification to something simpler, though. And leave out things like Falsehood, which I believe Tim has also abandoned. I'll check with him on getting it removed from http://www.w3.org/DesignIssues/Notation3.html. > So, just what am I allowed to use? What meaning am I to assign to the > semi-logical constants (like log:implies)? You're allowed to use N-Triples with literals, bNodes, and URI-Refs which will just be logical constants to the reasoner. (Syntactically distinct literals denote distinct objects, as usual.) In addition, you can use the normal (1,2,3) rdf:subject rdf:predicate rdf:object to describe an n3 atomic Formula, and you can use (4) log:conjunction, whose domain is a DAML list of 2+ formulas and range is the formula which is their conjunction. (Alternatively, we could allow log:and, which is true iff both its subject and object are true formulas. Such an approach would be more in keeping with this less-reified style.) => So { <a> <b> <c>. } is equivalent to _:x where _:x rdf:subject <a>. _:x rdf:predicate <b>. _:x rdf:object <c>. and { <a> <b> <c>. <d> <e> <f>. } is equivalent to _:y where _:y log:conjunction _:list. _:list daml:first _:x. # as above _:list daml:rest _:list2. _:list2 daml:first _:z. _:list2 daml:rest daml:nil. _:z rdf:subject <d>. _:z rdf:predicate <e>. _:z rdf:object <f>. Feel free to use { } terms using this meaning. (5) log:implies, whose domain and range are both formulas and means about what you think it does. (That is, the triple is known true iff its object (3rd element) is known true or its subject is not known true. I hope that's phrased right; I don't want to really introduce negation here. Maybe it would be better to phrase this as a rule than as material implication. (6,7): log:forSome and log:forAll, each of whose domain is a formula and whose range is unlimitted. These quantifiers act like this: the triple _:formula1 log:forAll _:var is true if and only if _:formula1 would be true for any consistant subsitution of _:var as an rdf:subject/predicate/object in the formula. More accurately, the substitution is of the object denoted by _:var, not the identifier text itself, which is not properly knowable, being syntactic rather than in the domain of discourse. (n3/cwm dithers about this, sometimes saying the quantifiers are syntax structures instead of plain triples; I believe the above is best, although somewhat non-traditional. I've heard people call it "possible worlds" semantics, but I don't know if that's appropriate.) log:forSome has no expressive power except inside the consequent/conclusion formula of log:implies. In much of the n3 written, people do things like "this log:forSome <x>." which seems much trickier, so I'm leaving it out. If we're safe without it, then we can consider adding it back. I think I need some clause about WFFs and self-reference, but I can't think of the right language. Something like: all the predicates involving formulas are not defined for ill-formed or self-referencial formulas. If that's where you want to push on the system, I'll try to be more precise. > Of course, I had to make a number of assumptions as to the meaning of n3 > constructs in the above argument. However, I feel that all my assumptions > are reasonable, given the available documentation on n3. Absolutely, and I have to apologize again for not being much more clear in my challenge. Even though TimBL has removed/never-implemented log:Falsehood, he has implemented and often uses log:notIncludes [2], which still supports forms of the liar paradox given its current documentation. It might possible to define it in some form that disallows loops, as I imagine the actual implementation does. My focus here is on something closer to propert Horn clauses. I'm using existentially quantified variables and allowing conjunctions in the consequent, instead of function terms and only an atomic sentence in the consequent, but I believe the forms are equivalent. -- sandro [1] http://www.w3.org/2001/12/semrun/test-conditional.rdf [2] midway down http://www.w3.org/2000/10/swap/log.n3
Received on Tuesday, 30 April 2002 07:07:03 UTC