Re: Explaining undecidability for RDF-based Semantics

Hey Bijan,

On 09/09/2015 17:43, Bijan Parsia wrote:
> Great thread!

:)

> Just to make sure I get the constraints:
>
> You want to explain why OWL Full is undecidable. Your students may
> not know what decidability is. They definitely won’t have any
> standard undecidable problems “in their hat” ready to go.

That's pretty much it yep!

> So, the challenge is: 1) To explain what it is to be undecidable. 2)
> Explain reduction style proofs 3) Explain a target undecidable
> problem. 4) Show the reduction for OWL 2 Full.
>
> This is a freaking lot! I mean, awesome, but a lot of a lot. Esp. if
> you want a reasonably worked out version of all the proofs. I
> personally suspect something has to give :)

Yes. I think (1) and (2) would be accessible enough just for the 
undecidability case. I guess what I was hoping for (but am starting to 
now lose hope for) was the existence of instances of (3) and (4) that 
were sufficiently accessible. I suspected that there may be some 
straightforward undecidability proof for entailment under the OWL 2 Full 
language (at least more straightforward than those published looking at 
specific features and specific DLs).

But yep, I am also starting to see that something has to give. :)

> I think the reduction to tileling is the best known reduction for
> showing stuff about property cycles. One nice thing is that it’s
> straightforward to add something that goes over the edge then show
> how a restriction pulls you back. Similarly, it’s a good way to get 2
> manners in which OWL Full is undecidable (unrestricted properties and
> alc + metamodelling).
>
> From a  practical perspective, doing *more* reductions is better than
> explaining the proof of the target problem. Reductions are the
> workaday proof method and the direct undecidiablity proofs seem
> rather challenging.

Yes, I think the tiling problem itself would be accessible enough but as 
you say, I'm afraid the reduction would be too much for students just 
starting to learn about OWL. Even if it's too much, I can still sketch 
the ideas of undecidability, of a reduction, and point to a few papers 
elsewhere with such reductions that would suffice.

What I like about the idea of showing the reduction and proving the 
undecidability of OWL 2 Full is giving the students a sense of the 
"power" of the language beyond some typical ontology modelling tasks ... 
using it to solves some really hard task ... something that may not be 
clear from the "declarative" nature of the language or to students with 
a more imperative outlook on life. Likewise it motivates the need for 
sub-languages, and the principles by which those sub-languages are designed.

If the best approach is to use a reduction from domino tiling, the 
challenge then is to find the right level/approach so that the students 
learn something without getting frustrated about the whole thing. :)

Cheers,
Aidan

Received on Thursday, 10 September 2015 22:09:41 UTC