Forcing a closed world assumption on an OWL class

Question

I have an OWL class with the following Equivalence (in Manchester notation):

A and not (hasB some (B and (hasC some C) and (hasD some D) and (hasList some (OWLList and (hasContents some (OWLList and (hasContents some (E and (hasValue some integer[< 200]) and (hasType value "xsd:integer"^^string))) and (hasNext some EmptyList))) and (hasNext some EmptyList)))))

I wish to enforce closed-world reasoning on this class so that any individual that does not fulfil the remainder of the condition after the not statement will be a member of this class.

To this end I have tried making the hasC, hasD and hasList properties functional so that OWL knows it is not possible for there to be other instances of these properties attached to this class.

Unfortunately it is possible for the hasB property to occur more than once so this cannot be restricted. To try and 'close' this part of the class I have added a oneOf statement in the B class specifying all possible individuals that the B class may accept.

To my mind this combination of Functional properties and oneOf statement should successfully 'close' the class. Can anyone advise me as to what I am doing wrong?

I am using the OWLList class and associated properties proposed by http://owl-workshop.man.ac.uk/acceptedLong/submission_12.pdf.

Many Thanks.

Answer 1

OWL is built on the open world assumption, and you can't really get around that. In some cases, you can provide some additional axioms about a class to reduce the number of possibilities that an open world permits. E.g., if you have

{d} ⊑ ∃ hasValue exactly 1 {a, b, c}
a ≠ b
a ≠ c
b ≠ c

then from hasValue(d,a), you could infer both of these:

¬hasValue(d,b)
¬hasValue(d,c)

What you're asking for sounds more like default reasoning where you're trying to say that

If X isn't provable using standard OWL, then infer ¬X.

The difficulty in this is that you can represent both positive and negative statements in OWL, and you'd have a problem when neither X not ¬X is provable using standard OWL, since in that case, you'd infer both ¬X and ¬¬X.

However, there are some things that you can do here. If you're generating the data, you can add negative property assertions to explicitly state that some particular relation doesn't hold. That's one way of encoding total knowledge about some subset of your domain. Thus, if there are a number of known B's out there, then you can assert for each one whether an A is related to each one or not.

Another option would be using SPARQL to query the data and check whether an A is related to a qualifying B, and if it's not, then add some additional data that will an OWL reasoner draw the inferences that you need. This isn't too hard, but if any of the other relations that need to find the B's that you're looking for are inferred, you still might need an OWL reasoner running prior to the SPARQL queries.

Answer 2

Stardog has a feature called Integrity Constraint Validation which adds a closed-world interpretation to OWL to be able to use it as a validation language. You can read more about how this is done in a detailed breakdown of the semantics.

I'm not sure if the validation part is what you're going for, but if so, you could use Stardog ICV straight away. And if not, the semantics might point you at how you can implement precisely what you need.