Re: Explaining undecidability for RDF-based Semantics

Hey Michael,

Thanks for the detailed response! :) Some comments in line.

On 06/09/2015 11:05, Michael Schneider wrote:
> 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.

Ah okay. For some reason I had it in mind that OWL Full drops the 
container membership properties (not sure why), but of course as an 
extension of RDFS, it would contain these properties.

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

Sure yep. My question is about the entailment problem, not about 
computing the closure (which was mentioned by Ignazio). I like the 
example you give. :)

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

Right! In terms of arguing that OWL Full is undecidable because some 
sub-language thereof is undecidable, didactically speaking, this simply 
moves the question from why OWL Full is undecidable to why some 
sub-language of OWL Full is undecidable. Of course, this is a problem 
with any "reduction" but I'd like to at least use a standard undecidable 
problem. Outlining the proof of Boris' paper would be perfect, but of 
course as you highlight, it may not be so accessible.

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

That's what I'm hoping for!

I had a quick look at trying to do a reduction from the Post 
Correspondence Problem (which as far as undecidable problems go, seems 
easy enough to explain ... and if there were an intuitive reduction to 
entailment with OWL 2 Full, it would suit my needs perfectly). 
Unfortunately it doesn't seem so trivial to develop. The rough idea was:

1) to use "recursive" some-values-from to create a tree of the words in 
the alphabet (take an alphabet of {a,b} and define S ⊑ ∃a.S, S ⊑ ∃b.S, 
S(root)),

2) to define specific words using property chain axioms ("aba" -> a ∘ b 
∘ a ⊑ p_1, "ba" -> b ∘ a ⊑ q_1),

3)  to try to use functional properties and/or "something else" to 
create a cycle (though same-as) if and only if there is a positive match 
to the PCP problem. The "something else" seems not to be so easy though.

4) See if hasSelf on some property is entailed on the root individual to 
check the cycle.

Step 3) doesn't seem so straightforward though. I was hoping that this 
proof might show why there are restrictions involving simple roles.

Anyways, thanks again for the response!

Cheers,
Aidan


> 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 Wednesday, 9 September 2015 19:44:07 UTC