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

Tim Glover wrote:

> 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 :-)

Oh yes, this is very interesting stuff to answer my original question! 
Google retrieved me the dissertation of Boris Motik, where I found the 
said proof in section 11.1:

http://www.ubka.uni-karlsruhe.de/cgi-bin/psview?document=2006/wiwi/1&search=%2f2006%2fwiwi%2f1&format=1&page=196

This is a very short (< 4 pages) and self contained section, so I was 
able to do a rather quick first read. Many thanks for this hint, Tim!

> 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

Well, from this proof I learned to know some very irritating properties 
of OWL-Full, which I wasn't aware of, yet. While one probably cannot 
define this "mean" Cantor set which I was talking about in my first 
post, very curious ontologies can be build within OWL Full, which no 
human ontology designer would actually call an "ontology" (IMHO). 
Perhaps, I should give a little overview of the proof as far as I 
understand it, to make clear what I mean by "curious ontologies".

Motik first introduces this "domino tiling" problem, for which it is 
known that it is undecidable: A "domino system" consists of a finite set 
of types of domino stones, say different stone colors, where there are 
arbitrary many (infinite) concrete stones for each color available. Such 
stones can be aligned horizontally and vertically, but only if this 
leads to some allowed combination of colors. Now, the task is to 
completely fill some infinite "Chess board" (infinite to the east and to 
the south, formally an NxN grid) with domino stones in an allowed way. 
There is no algorithm which can tell, if for a given domino system 
(stone types plus color combination constraints) there exists such an 
allowed filling (or "tiling").

Now comes the smart part: Motik constructs some OWL Full ontology 
(actually, a sub language of OWL Full is used to make the proof clearer) 
for each possible domino system, in a way, that the constructed ontology 
is actually an encoding of the domino system in OWL Full. Next, Motik 
shows that for every such constructed ontology, each of its possible 
interpretations formally has the structure of an allowed Chess board 
tiling for the encoded domino system. So, it is finally shown that the 
problem of satisfiability for a special set of OWL-Full ontologies ("Is 
there some interpretation for a given ontology?") is equivalent to the 
domino tiling problem. And because the latter problem is undecidable, so 
is the satisfiability problem for OWL full.

So, while I hold the proofing idea alone for quite amazing, see how the 
encoding ontologies are constructed! Each such ontology consists of 
about a dozen axioms, most of them I would call "complete nonsense" 
(from a pragmatical view), though they are indeed allowed (they have a 
semantics). E.g., there is some axiom of the form

     GRID rdfs:subClassOf owl:allValuesFrom .

Here, the set GRID is not interesting for our discussion, but look, what 
the hypernym of GRID is: 'owl:allValuesFrom'. Uh, what? And in another 
axiom, Motik makes the relations 'rdf:type' and 'owl:onProperty' as 
synonyms:

     rdf:type owl:sameAs owl:onProperty .

The amazing thing with this assertion is, that it is really important 
for Motik's proof to work.

So, to come back to my original post, I was looking for a nice example, 
which shows me, why OWL Full is not decidable. I speculated that it must 
have something to do with the possibility to make classes instances of 
other classes. But I had not expected what kinds of "exciting 
possibilities" OWL provides, which then must[?] be exploited to show the 
result. Welcome to the dark side of OWL! ;)

Cheers,
Michael

Received on Tuesday, 7 November 2006 22:26:59 UTC