W3C home > Mailing lists > Public > www-archive@w3.org > January 2002

Re: Grist for layering discussion

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
Message-Id: <20020112064309C.pfps@research.bell-labs.com>
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.


Received on Saturday, 12 January 2002 06:44:02 UTC

This archive was generated by hypermail 2.3.1 : Wednesday, 7 January 2015 14:42:04 UTC