W3C home > Mailing lists > Public > www-webont-wg@w3.org > November 2002

Re: Sketch: reasoning conformance levels

From: Ian Horrocks <horrocks@cs.man.ac.uk>
Date: Thu, 7 Nov 2002 20:04:34 +0000
Message-ID: <15818.51026.266747.115039@merlin.horrocks.net>
To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
Cc: welty@us.ibm.com, www-webont-wg@w3.org

On November 7, Peter F. Patel-Schneider writes:
> 
> From: Christopher Welty <welty@us.ibm.com>
> Subject: Re: Sketch: reasoning conformance levels (was RE: Issue: Add hasValue to OWL Lite)
> Date: Thu, 7 Nov 2002 11:23:03 -0500
> 
> > 
> > I don't think there is any reason to say OWL Full is not for reasoners, 
> > nor have I seen any evidence to date that OWL Full is incomplete, though 
> > I've noticed several messages that seem to take it for granted.  
> 
> Well, it doesn't make much sense to describe a semantics as incomplete in
> this context, and, in any case, I think that the OWL/Full semantics is no
> different from the OWL/DL semantics in this respect.
> 
> > In fact, 
> > I believe OWL Full is sound and complete, though intractable as all hell 
> > I'm sure. 
> 
> More accurately, entailment in OWL/Full is (likely) undecidable and not
> amenable to complete implementation by DL reasoners.  (I seem
> to remember arguments, perhaps even by me, that it *is* undecidable.)  

Given that the side-condition on the use of transitive roles in number
restrictions does not apply to OWL Full, then it is certainly
undecidable. You can look in [1] for a proof. I'm sure it would also
be possible to prove some other cause of undecidability.

Ian

[1] http://www.cs.man.ac.uk/~horrocks/Publications/download/1999/lpar99.ps.gz


> 
> > Therefore I believe the only thing we can say about OWL Full, wrt 
> > reasoning and reasoners, is that no one knows how to build a reasoner that 
> > supports all of OWL Full.
> 
> Actually, it should be possible to build a complete (one-sided) reasoner
> for OWL/Full as entailment in OWL/Full is semi-decidable.  Just axiomatize
> in SKIF and then axiomatize the resulting SKIF in standard FOL and use a
> complete FOL reasoner.  I don't expect to see blazing performance, however,
> :-)
> 
> > Dr. Christopher A. Welty, Knowledge Structures Group
> > IBM Watson Research Center, 19 Skyline Dr.
> > Hawthorne, NY  10532     USA 
> > Voice: +1 914.784.7055,  IBM T/L: 863.7055
> > Fax: +1 914.784.6078, Email: welty@us.ibm.com
> 
> peter
Received on Thursday, 7 November 2002 15:04:55 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:55 GMT