RE: Undecidability of OWL-Full and Cantor's antinomy

PS
 
I think the "domino" example shows that the issue in OWL-FULL is the (rather eccentric!) lack of distinction between the language and the meta language, which makes it possible to change the meaning of language terms like owl:Class
 
T.  

 -----Original Message----- 
 From: Glover,T,Tim,CXR3 R 
 Sent: Tue 07/11/2006 10:29 
 To: Michael Schneider; pfps@research.bell-labs.com 
 Cc: W3C SWIG Mailing-List 
 Subject: RE: Undecidability of OWL-Full and Cantor's antinomy
 
 
 Michael,
  
 Boris Motik constructed a good example showing the undecidablility on OWL full using a "domino tiling" problem which is known to be undecidable. I don't have web access at the moment, but I expect Google could help locate the paper :-)
  
 Tim Glover

  -----Original Message----- 
  From: semantic-web-request@w3.org on behalf of Michael Schneider 
  Sent: Tue 07/11/2006 09:36 
  To: pfps@research.bell-labs.com 
  Cc: W3C SWIG Mailing-List 
  Subject: Re: Undecidability of OWL-Full and Cantor's antinomy
  
  


  Peter F. Patel-Schneider wrote on 2006-11-04:
  
  > I believe that you are going down the wrong path here.
  >
  > Your argument goes more towards semantic paradox than decidability.  If the
  > bad set was present in all OWL Full semantic structures, then the meaning
  > of OWL Full would collapse.  However, OWL Full was carefully engineered to
  > avoid many of the common semantic paradoxes, and thus only certain kinds of
  > "sets" are present in all OWL Full semantic structures.
  
  Aha, I did not know this! Until now, I had in mind some vague concept of
  the form "in OWL-Full I can express whatever I want", and that it would
  be up to me to not write down nonsense (like I actually /can/ write down
  this Cantor's set in mathematics, because it is /syntactically/ a well
  formed expression, but, as I understand it, it simply does not have any
  meaning in mathematics).
  
  In most cases, when thinking about some distinctive difference between
  OWL-Full and DL, I had in mind this
  
     owl:Class rdf:type owl:Class .
  
  triple, which means that in OWL-Full a class can be an instance of
  itself. And if this is allowed, than the following should also be allowed:
  
     owl:Class rdf:type [ owl:complementOf owl:Class ] .
  
  and this, as you might guess, finally took me to the idea of defining
  the "bad" Cantor set.
  
  But, ok, from what you said this probably won't work, and this is, of
  course, a good thing. :)
  
  Thanks for your reply!
  
  Michael
  
  
  > From: "Michael Schneider" <m_schnei@gmx.de>
  > Subject: Undecidability of OWL-Full and Cantor's antinomy
  > Date: Fri, 3 Nov 2006 18:01:26 -0600
  >
  >> Hi!
  >>
  >> I recently read the discussion about undecidability of OWL-Full, which
  >> took place here several weeks ago in thread
  >>
  >>     "Readings on OWL's (un)decidability?"
  >>
  >>     From: Yoshio Fukushige <fukushige.yoshio@jp.panasonic.com>
  >>     Date: Mon, 02 Oct 2006 15:28:15 +0900
  >>     URL: http://lists.w3.org/Archives/Public/semantic-web/2006Oct/0005.html

  >>
  >> Well, I have never before dealt with this issue, so after reading the
  >> thread, I tried to make up some good example which might help me to
  >> better understand this "undecidability problem" in OWL-Full. I finally
  >> came up with the idea to define within OWL-Full Cantor's well known set
  >> of all those sets, which do not have them self as an instance:
  >>
  >>     (1) C := { m | m NOTIN m }
  >>
  >> where "NOTIN" means "is not an instance of". This definition is
  >> equivalent to
  >>
  >>     (2) C := { m | m IN \m }
  >>
  >> where "\m" denotes the complement of m. The problem with this set
  >> becomes obvious when one asks, if C is an instance of itself, or not:
  >>
  >>     (3) C IN C <==> C IN { m | m IN \m } <==> C IN \C <==> C NOTIN C
  >>
  >> So from the definition of set C one can conclude a contradiction. And
  >> this means that, if one defines this set within some OWL ontology, there
  >> is some query of the form "Is x in M?" (with x = M := C), which cannot
  >> be answered by any algorithm. Thus, OWL-Full would be undecidable.
  >>
  >> First, it is clear that one can *not* create such a definition within
  >> the DL dialect of OWL: The variable m from the expression "m IN \m" must
  >> be an owl:Class, because only for a class m it is allowed to build its
  >> complement "\m". So, one would have to create a statement like (in N3
  >> notation):
  >>
  >>     (4) :m rdf:type [ owl:complementOf :m ] .
  >>
  >> where both :m and "[ owl:complementOf :m ]" are classes, and this is not
  >> allowed in OWL-DL.
  >>
  >> But this would not be a show stopper within OWL-Full, where a class
  >> *can* be an instance of another class. So the question remains,
  >> how to define the class C in OWL-Full in an analog way to eq.(2) above?
  >> Looking at eq.(4), I was thinking about defining some owl:Restriction on
  >> property 'rdf:type', so C would become something like:
  >>
  >>     (5) :C a owl:Class ;
  >>           owl:equivalentClass [ a owl:Restriction ;
  >>             owl:onProperty rdf:type ;
  >>             owl:allValuesFrom [ owl:complementOf :m ]  # WRONG!
  >>           ] .
  >>
  >> Of course, this does not work, because this expression has another
  >> meaning than the expression in eq.(2): Eq.(5) would mean:
  >>
  >>     C is the class of all those things x,
  >>     which are instances of the complement of some _named_ class ':m'.
  >>
  >> But in eq.(2), 'm' does not stand for some named class, but is a _bound_
  >> variable within the class expression. Now, I do not see any possibility
  >> in OWL-Full to do something like using named bound variables, like 'm'
  >> in eq.(2). Does anybody has a clue how to define the Cantor set in
  >> OWL-Full?
  >>
  >> Or, perhaps, it might come out that this isn't possible at all? As far
  >> as I understand, for being undecidable, it is demanded that there is no
  >> single algorithm, which for every pair of ontologies O1 and O2 correctly
  >> states if O1 entails O2, or not. Sounds like that there must at least
  >> /exist an answer/ (either "true" or "false"), which simply is /not
  >> computable/. But in my example above, there /doesn't even exist/ any
  >> answer to the question "C IN C?".
  >>
  >> Any ideas, to bring some light to my question?
  >>
  >> Cheers,
  >> Michael
  >>

Received on Tuesday, 7 November 2006 10:35:22 UTC