Re: post-conditions in OWL files

At 6:56 PM +0000 2/27/08, Matthew Pocock wrote:
>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.

Wrong thinking (if you will forgive the adhominism). The SWeb 
language specs are very careful to not say anything normative about 
processing mechanisms. You are free to do what you like with OWL, 
provided that it respects the normative semantics: and that only 
specifies what the conditions are for a sentence to be true.

>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)

What you should say is what the spec says you can infer, to wit: 
SubClass(uncle brother).

>Post-reasoning, for the ontology to be consistent, this assertion MUST be
>satisfied.

? No. Obviously an ontology can be *consistent* without entailing 
this. I suspect you mean something other than 'consistent' here.

>If not, then there is a problem.

OK, lets just agree on that, but its a problem for you, not for OWL.

>  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.

Semantically there really is no difference. Any difference you want 
to record is therefore outside the scope of the OWL spec.
BTW, why would this necessarily be an 'input axiom' ? THeres nothing 
in OWL that says it can only be used for input to a reasoner.

>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.

Fine: go ahead and do one of these. You are here working (just) 
outside the scope of the OWL spec as written, but that is fine as 
long as you don't claim that any extended meaning is a genuine OWL 
entailment.

>  It would, however, make managing ontologies that rely heavily on
>computational support much easier, especially if tools and reasoners groked
>it

... Ah. If you want other people's tools to grok your particular 
extended meanings, that is asking a bit too much.

>, and if we could keep these required entailments close to the axioms they
>refer to.

Again, that is up to you, the spec simply is silent on such 
implementation matters.

Pat

>
>Matthew


-- 
---------------------------------------------------------------------
IHMC		(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32502			(850)291 0667    cell
http://www.ihmc.us/users/phayes      phayesAT-SIGNihmc.us
http://www.flickr.com/pathayes/collections