- From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
- Date: Sat, 12 Jan 2002 06:43:09 -0500
- To: connolly@w3.org
- Cc: timbl@w3.org, sandro@w3.org, phayes@ai.uwf.edu, hendler@cs.umd.edu, las@olin.edu, w3c-semweb-ad@w3.org, www-archive@w3.org
From: Dan Connolly <connolly@w3.org> Subject: Re: Grist for layering discussion Date: 11 Jan 2002 20:46:44 -0600 > On Fri, 2002-01-11 at 19:14, Peter F. Patel-Schneider wrote: > [...] > > > So you feel that allowing reification -- or, presumably, allowing > > > sets of statements as first class objects in the syntax -- makes the system > > > such that one can necessarily deduce a contradiction from nothing? > > > Then I need help understanding how. > > > > Look at the spec for KIF at http://logic.stanford.edu/kif/dpans.html. The > > section on Metaknowledge has a nice description of one such problem. > > A solved problem, no? Well, yes, as long as you don't mind the effects of the solution, which are to, roughly, disallow any ``formula'' that is self-referential. Unfortunately, there are lots of such situations that are needed. (In KIF, the problem only occurs with respect to WTR, because that is the predicate that asks whether a ``list'' represents a true formulae. In the DAML+OIL case, however, there is essentially an implicit WTR attached to every restriction.) > I've looked at it... several times. It seems to be exactly > what we need. (Actually, the KIF v3 version is less constraining > and looks more useful). One way of translating the KIF solution to DAML+OIL would end up disallowing classes from belonging to themselves, even indirectly. I don't think that you want that. > But metaknowledge aside... > > I'm still trying to figure out why the axiomatic semantics > for DAML+OIL isn't perfectly good basis for WebOnt. It > seems to play nicely with the RDF model theory, as far as > I can tell. That is: the RDF model theory gives > an n-triples document (and hence any RDF document) > a meaning that corresponds > directly to a KIF formula of the form > > (exists (?x1 ?x2 ?x3) > (and > (p1 s1 o1) > (p2 ?x1 o2) > (?x3 s3 o3) > ... > ) > ) > > I trust you'll grant me that (PropertyValue p s o) isn't > interestingly different from (p s o) with the menzel indirection trick, > no? > > What's wrong with specifying ont:complementOf ala: > > (forall (?C1 ?C2) > (iff (ont:complementOf ?C1 ?C2) > (forall (?x) > (iff (rdf:type ?x ?C1) (not (rdf:type ?x ?c2))) > ) ) ) > > How does the model theory paradox you presented earlier show > up in an axiomatic specification like this? You end up with an inconsistent axiomatization. Not from things like the above, of course, but from self-referential structures, in which you can, roughly, say if x belongs to y, then x does not belong to y if x does not belong to y, then x does belong to y The problem with the current specifications of DAML+OIL, both the model theory and the axiomatization, is that they don't work the same way as the RDF model theory. This is fine, but then DAML+OIL and RDF(S) are different. If you want this, then there is no problem, but you have lost the extension relationship between RDFS and DAML+OIL. If making DAML+OIL (or OWL) an extension of RDF(S) is dropped from our list of desirables, then there are lots of changes that I have to make DAML+OIL (or OWL) better. [...] > > > > Why is there a problem? The problem arises, as Pat has stated, from the > > > > attempt to extend a representation formalism while not extending the > > > > syntax. This cannot be done in many circumstances and can only be easily > > > > done in very limited circumstances. > > > > > > I need to understand better where the problem lies. > > > > Unfortunately, understanding the problem does require groking some > > interesting logical notions. > > I think I grok the relevant stuff... from what I can tell, > you do have to be a bit careful, but it's not impossible. > KIF's wtr is an example of a solution, no? See above. > i.e. TimBL's log:Truth is pretty much the same thing > as KIF's wtr. And log:implies works sorta like: > > (defrelation (log:implies ?P ?Q) <=> > (wtr '(implies ,?P ,?Q)) Well, not really. If ?P or ?Q contain log:implies, the wtr solution will certainly not be what you want. As long as you can't create a contradiction, all this reification stuff usually works fine. However, contradictions and reification generally allow you to create the Liar's paradox, and everything comes tumbling down. [...] peter
Received on Saturday, 12 January 2002 06:44:02 UTC