From: Michael Schneider <m_schnei@gmx.de>

Date: Sun, 6 Sep 2015 16:05:49 +0200

To: Aidan Hogan <ahogan@dcc.uchile.cl>, public-owl-dev@w3.org

Message-ID: <55EC483D.1020507@gmx.de>

Date: Sun, 6 Sep 2015 16:05:49 +0200

To: Aidan Hogan <ahogan@dcc.uchile.cl>, public-owl-dev@w3.org

Message-ID: <55EC483D.1020507@gmx.de>

Hi Aidan! First to say that, yes, OWL Full /does/ cover all the container membership properties, and for obvious reasons, because the semantics of OWL Full is a semantic extension of the semantics of RDFS, and it applies to the same syntax as RDFS. However, as Pat pointed out, the infinity of the entailment closure due to the infinite number of these properties does not necessarily lead to undecidability, as it becomes clear from RDFS, which /is/ decidable. In general, it is easy to receive infinite entailment closures in decidable languages by adding some more logic constructs to it. For example, in OWL DL, which is a decidable language, you have an infinite entailment closure for the empty ontology (and thus for every ontology) consisting of many trivial statements, such as {} |= { C subClassOf ( C union C ) ; C subClassOf ( C union C union C ) ; ... } The impossibility of computing the whole entailment closure for any RDF graph G in finite time is not the same as undecidability of the entailment problem. The latter is the impossibility to create an algorithm A such that for every syntactically valid pair of input graphs G and G', A is guaranteed to terminate after finite time and will correctly tell whether G entails G' or not. Of course, /if/ you can compute the complete entailment closure for any given graph G in finite time, /then/ you can easily build a a decision algorithm based on this, by simply checking whether your target graph G' is a subset of the resulting entailment closure or not. But this approach is only possible for very inexpressive entailment regimes, and it will usually be kind of the most inefficient decision algorithm one could think of, both regarding time and space consumption. Now to the question "why is OWL Full undecidable". You point to Boris' Motik's paper, and the proof that you are citing from this paper provides /one/ of the reasons why OWL Full is undecidable. This proof shows that, due to the freedom given by the RDF semantics to use language terms such as rdf:type, rdfs:subClassOf, etc, like normal entities (properties, classes, individuals), the RDF semantics becomes undecidable very quickly if one only adds some more logic constructs to it: this proof is really the much smaller semantic fragment of OWL Full called "ALCO Full" (w/o datatypes), which corresponds to ALCO, a very basic decidable description logic. If you want to use this particular argument to explain undecidability of OWL Full to your students, then, I'm afraid, you have to go down the - ingenious but hard to understand - path Boris used in his proof, as I haven't heard of any simplification of his proof yet. However, this is not the only reason why (the whole of) OWL Full is undecidable, and Boris' paper points this out as well. Here is a simple, informal argument that may already be of use for your teachings: OWL (2) Full "simulates" OWL (2) DL, as close as the concepts of the RDF semantics allows, but OWL Full doesn't use the syntactic restrictions that have been added to OWL DL in order to remain decidable. Hence, it should be clear that OWL Full must be undecidable. In fact, if you apply the OWL 2 Direct Semantics to the unrestricted(!) OWL 2 Abstract syntax, i.e., the language consisting of OWL 2 DL but without all the syntactic restrictions that have been added to OWL 2 DL to retain undecidability (this includes the "Global Restrictions on Axioms in OWL 2 DL" in Chapter 11 of the OWL 2 Structural Specification), then this extension language of OWL 2 DL" becomes undecidable - and this extended language is still even less expressive than OWL 2 Full! You can go further and check through the list of syntactic restrictions that are used in OWL DL in order to retain decidability, and find one(!) such syntactic restriction for which undecidability under the OWL Direct (!) Semantics can be particularly easy shown and understood. Essentially the same undecidability reason should then hold for OWL 2 Full as well (doing proofs directly about OWL 2 Full can be pretty nasty at times). I haven't yet analysed OWL DL under such a didactic point of view and feel a little lazy to do so now, so I will leave this to yourself or to some of the description logic experts here to find out. In any case, however, I believe it to be unlikely that you can avoid any of the usual formal approaches to proving undecidability of formal languages, be it either directly by applying some sort of diagonalisation argument, or indirectly by using a reduction, like in the case of the domino tiling problem in Boris' paper. But on the other hand, you should in this way really find some proof that is considerably easier to understand than the one in Boris' paper, at least. :-) Michael Am 04.09.2015 um 21:53 schrieb Aidan Hogan: > Hi all, > > I'm teaching some Semantic Web stuff and I was looking for as > simple/intuitive/direct an explanation as possible as to why (e.g.) > entailment checking under OWL 2 RDF-Based Semantics is undecidable, and > why it thus may be desirable to define a restricted semantics/language. > > > I know, for example, that there are reductions from the Domino Tiling > problem using features in OWL (2) Full such as metamodelling involving > the OWL vocabulary itself, or complex roles in number restrictions: > > Boris Motik: > On the Properties of Metamodeling in OWL. J. Log. Comput. 17(4): 617-637 > (2007) > > I. Horrocks, U. Sattler, and S. Tobies. > Practical Reasoning for Very Expressive Description Logics. Logic > Journal of the IGPL, 8(3):239–263, 2000. > > ... but again, I'm hoping (if possible) to find something much more > simple/didactic, perhaps exploiting some other well-known decidability > restriction that OWL 2 Full misses and/or a reduction from an even > "simpler" undecidable problem. (It is quite possible I'm missing > something obvious.) > > > Any pointers or ideas would be great. The target audience would be > undergrads who may not have taken a logic or complexity course. The goal > is to establish the undecidability of entailment for OWL 2 Full in as > accessible a manner as possible. > > Best, > Aidan >Received on Sunday, 6 September 2015 14:06:40 UTC

*
This archive was generated by hypermail 2.3.1
: Sunday, 6 September 2015 14:06:41 UTC
*