Re: Grist for layering discussion

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