Re: Explaining undecidability for RDF-based Semantics

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