Re: Explaining undecidability for RDF-based Semantics

On Sep 4, 2015, at 3:18 PM, Ignazio Palmisano <ipalmisano.mailings@gmail.com> wrote:

> On 4 September 2015 at 20:53, Aidan Hogan <ahogan@dcc.uchile.cl> wrote:
>> 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.)
>> 
> 
> I'm no expert on the topic but I've spotted the following:
> 
> http://www.w3.org/2009/12/rdf-ws/papers/ws16
> 
> A one sentence explanation of undecidability is included: given that
> the definition of entailment says that the RDFS container membership
> triples must be included in the entailment graphs, and the set of
> container membership triples is infinite, the entailment graphs have
> infinite size.

That does not, however, make RDFS entailment undecideable. (And the revised RDF 1.1 spec removes this inelegance, by the way.)
Undecideabilty of OWL is ultimately due to the undecideability of first-order logic, which is reducible to the same basic idea for why it is uncomputable whether or not a Turing machine halts. 

> As I understand from other articles as well (can't find the full text
> for them though), this undecidability can be avoided (by skipping the
> infinitely many triples whose property does not appear in the actual
> graph under examination, i.e., all rdf:_i properties such that there
> is no collection with an ith element in the graph are discarded.).

Yes, exactly. 
> 
> This is just one example of an avoidable undecidability :-)

You have the wring idea about undecideability. It is not something that can be avoided: sufficiently expressive logics are undecideable not because of any defect in some set of rules, but because the set of sentences that are logically true is uncomputable, basically because the logics are able to express something which means "this sentence is unprovable", which (if the logic is internally consistent) has to be unprovable, and is therefore true. 

Pat 

> I reckon I
> would have enjoyed such a presentation in my student days.
> Cheers,
> I.
> 
>> 
>> 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
>> 
> 
> 

------------------------------------------------------------
IHMC                                     (850)434 8903 home
40 South Alcaniz St.            (850)202 4416   office
Pensacola                            (850)202 4440   fax
FL 32502                              (850)291 0667   mobile (preferred)
phayes@ihmc.us       http://www.ihmc.us/users/phayes

Received on Friday, 4 September 2015 21:49:21 UTC