Re: owl 1.0 DL implementation experience

Hi Jeremy!

On 12 Feb 2007, at 15:53, Jeremy Carroll wrote:

> Another simple question reflecting me having been somewhat out-of- 
> touch (particularly having been off sick)
>
> When OWL went to Rec there was still some gaps in the  
> implementation experience with OWL DL 1.0. In particular, iirc,  
> there were some gaps in the completeness of support for reasoning  
> with nominals.
>
> By understanding is that pellet addressed these. Is that correct?

Ian Horrocks and Uli Sattler came up with a tableaux based decision  
procedure for SHOIQ (a superset of OWL DL),

	<http://www.cs.man.ac.uk/~sattler/publications/shoiq.pdf>

  and there is an extension of that for SROIQ (roughly OWL 1.1).

	<http://www.cs.man.ac.uk/~sattler/publications/sroiq-tr.pdf>

Both FaCT++ and Pellet have implemented this algorithm for quite some  
item (Pellet was first by a bit and it's been there for over a year).  
They both now implement SROIQ (though FaCT++ was first here :)).

There are a suite of  optimizations for nominals described in:
	<http://www.mindswap.org/papers/2006/KR0603SirinE.pdf>

which have been implemented in Pellet and do quite well. FaCT++  
implements a few and is experimenting with others, but never the less  
is able to handle the Wine ontology (which is the most complex  
nominal example around, really) in reasonable time (about a minute on  
stock hardware).

> Are there a number of OWL DL 1.0 implementations that provide sound  
> and complete terminating reasoning for all input (of not  
> unreasonable size), with practical performance as in horrocks' use  
> of practical in 'practical reasoning' papers?

Yes. See Pellet and FaCT++. I believe Racer will follow but as they  
are in a rather demanding commercial setting, they tend to lag a bit  
on er...nominal completeness :) (in favor of extensions).

KAON2, I believe, won't support nominals anytime soon, as it's  
particular procedure (resolution via reduction to disjunctive  
datalog) doesn't obviously easily extend to nominals. However, there  
is the very interesting resolution procedure:
	<http://www.cs.man.ac.uk/~bmotik/publications/papers/km06shoiq.pdf>

I'll note that Arity is also working on a (commercial) SROIQ reasoner:
	<http://lists.w3.org/Archives/Public/public-owl-dev/2007JanMar/0031>

They also have an EL++ paper which allows for (restricted, but true)  
nominals in a worst-case polynominal time decision procedure setting:

	<http://owl1_1.cs.manchester.ac.uk/tractable.html#2>

So, one reason to extend the overall language is if there were  
interesting and used fragments that had extra features. See EL++.  
It's nice to have expressive, tractable, useful fragments *and* an  
umbrella language.

> It's fairly easy to encode quite difficult problems into OWL DL,  
> and I assume that good implementations not only need things like  
> failure directed backtracking, but also using techniques like the  
> study of automorphism groups, to reduce the search space.

Er...I don't know. See the papers :)

Hope this helps.

Hope you are feeling better and stay that way!

Cheers,
Bijan.

Received on Monday, 12 February 2007 19:27:55 UTC