- From: Bijan Parsia <bparsia@cs.man.ac.uk>
- Date: Wed, 9 Sep 2015 21:43:52 +0100
- To: Aidan Hogan <ahogan@dcc.uchile.cl>
- Cc: Owl Dev <public-owl-dev@w3.org>
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. 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 :) 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. Cheers, Bijan.
Received on Wednesday, 9 September 2015 20:44:21 UTC