W3C home > Mailing lists > Public > semantic-web@w3.org > November 2006

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

From: <tim.glover@bt.com>
Date: Tue, 7 Nov 2006 10:35:06 -0000
Message-ID: <22662A3D243F5343A3C24A4012A78DB208026AEC@i2km05-ukbr.domain1.systemhost.net>
To: <tim.glover@bt.com>, <m_schnei@gmx.de>, <pfps@research.bell-labs.com>
Cc: <semantic-web@w3.org>
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

	-----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
	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!
		> 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

This archive was generated by hypermail 2.4.0 : Tuesday, 5 July 2022 08:44:58 UTC