post-conditions in OWL files

Hi,

We're using reasoners (dl and starting to look at dl-safe rules) very heavily 
now. Quite a large proportion of the 'structure' or our ontologies are now 
inferred from property restrictions rather than asserted explicitly. This is 
great in one way - we spend much more time thinking about manageable lumps of 
our application domains. However, it does lead to maintainance issues of its 
own.

What we are looking for is some sort of relaxed subClass that acts as a 
post-condition on the reasoner as a validity constraint. For example,

subClass(uncle male)
subClass(uncle (hasSibling some hasChild some Thing))
subClass(brother (male ^ hasSibling some Thing))

Now, I'd like to say in the ontology:

inferedSubClass(uncle brother)

Post-reasoning, for the ontology to be consistent, this assertion MUST be 
satisfied. If not, then there is a problem. However, this is weaker in one 
sense than asserting

subClass(uncle brother)

which would add this as a one of the input axioms of the reasoner, potentially 
raising an inconsistency if this clashes with other axioms. The 
inferredSubClass axiom would only raise inconsistency if it is not entailed 
by the other axioms.

I am fairly mechanism-neutral about this - it could be a seperate OWL file 
marked as 'required entailments' or some flag on axioms 'asserted, entailed' 
or whatever. It would, however, make managing ontologies that rely heavily on 
computational support much easier, especially if tools and reasoners groked 
it, and if we could keep these required entailments close to the axioms they 
refer to.

Matthew

Received on Wednesday, 27 February 2008 18:57:19 UTC