Proposed Test: oneof/inverse

I'd like to propose the following test that exercises the interaction of
one-of and inverse. A spy point is defined that everything in the domain
is related to. A restriction on the spy using an inverse property then
restricts the cardinality of the domain to being 2, which leads to the
unsatisfiability of "Unsatisfiable".

[Namespaces:
  rdf   = http://www.w3.org/1999/02/22-rdf-syntax-ns#
  xsd   = http://www.w3.org/2001/XMLSchema#
  rdfs  = http://www.w3.org/2000/01/rdf-schema#
  owl   = http://www.w3.org/2002/07/owl#
  a     = http://oiled.man.example.net/test#
]

Ontology(

 Class(a:Unsatisfiable partial
  restriction(a:r minCardinality(3)))
 Class(owl:Thing partial
  restriction(a:p someValuesFrom oneOf(a:spy)))

 ObjectProperty(a:invP)
 ObjectProperty(a:p
  inverseOf(a:invP))
 ObjectProperty(a:r)

 Individual(_:x
  type(a:Unsatisfiable))

 Individual(a:spy
  type(restriction(a:invP maxCardinality(2)))
  type(owl:Thing))

)

Manifest and RDF version attached (as proposed 035 in the dl tests).

Cheers,

	Sean


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

Received on Thursday, 3 July 2003 09:50:43 UTC