- From: Michael Schneider <m_schnei@gmx.de>
- Date: Tue, 07 Nov 2006 23:26:40 +0100
- To: tim.glover@bt.com
- CC: semantic-web@w3.org, pfps@research.bell-labs.com
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