Re: Need a test -- inverse and oneOf

On Wed, 11 Jun 2003, Jim Hendler wrote:

>
> To be able to close some of our LC comments, there must be a test in
> our test suite that includes both inverse and oneOf.  In an earlier
> message I outlined a simple one, but perhaps someone in the WG can
> come up with a better one.  It is my opinion that without such a test
> we will have trouble convincing some people that OWL DL is
> implementable (cf the comments from Jena and HP).  Can we please get
> such a test at least proposed??
>   thanks
>   JH

How about the following?

Ontology(

 Class(a:NiceCorporation partial
  restriction(a:employs allValuesFrom a:NiceGuy)
  restriction(a:employs someValuesFrom oneOf(a:tom a:dick)))

 Class(a:NiceGuy)

 ObjectProperty(a:employedBy
  inverseOf(a:employs))
 ObjectProperty(a:employs)

 Individual(a:dick
  type(complementOf(a:NiceGuy)))

 Individual(a:niceCorp
  type(a:NiceCorporation))

 Individual(a:tom
  type(restriction(a:employedBy allValuesFrom complementOf(a:NiceCorporation))))

)

The interaction of the oneof and the assertion that dick isn't a Nice Guy
allows us to conclude that niceCorp must employ tom. But then we know that
anything that employs tom cannot be a NiceCorporation (due to the
inverse), so we get an inconsistency.

It's pretty trivial, but I think you do need both one-of and inverse to be
able to state it.

	Sean


-- 
Sean Bechhofer
seanb@cs.man.ac.uk
http://www.cs.man.ac.uk/~seanb

Received on Wednesday, 11 June 2003 08:16:01 UTC