Re: post-conditions in OWL files

Firstly, thanks to everyone who has replied to this, both on and off the list. 
I think part of my problem was that I didn't know what words to google for, 
as ever.

On Wednesday 27 February 2008, Bijan Parsia wrote:
> Matthew,
>
> It sounds like you (roughly) want something like unit tests. Well a
> bit more general than that, but it's similar in spirit.

Yeah, I guess the unit-test thingies are also documentation of the intent of 
the modeller rather than purely checks-and-ballances, but that's besides the 
point for the logic itself.

> I'd use annotations on the axioms. Then it's easy enough to flush out
> the ones that should be verified rather than the ones that should be
> used.  Since this is only a development time matter (i.e., I presume
> it doesn't matter to a shipping app that C subClassOf D is asserted
> rather than inferred...in fact, having the asserted one is way faster!)

OK, so we would post-process the file to split it into two axiom sets and then 
make sure that the 'please entail this' set was actually entailed by the 
other. That sounds workable. 

> I've been wanting this for a while...so maybe I'll cook something up.
> In particular, Matthew Horridge and I have been discussing a lint
> tool that looked at all the justificaitons for all the subsumptions
> and reported ones whose only explanation was the singleton set
> contain itself. So, for example, suppose in some ontology O, the set
> of justifications for C sub D was:
> 	{{C sub D}}
>
> The lint tool would raise a fuss ("Hey, you're a lazy modeller,
> y'know?"). However, if the set were:
>
> 	{{C sub D}
> 	{C sub E. E sub D}}
>
> It'd be fine.

This would be a useful QC tool. I think some styles of ontology building 
encourage the maximisation of these singleton justifications - I'm thinking 
BFO here. So, one way or the other, it could turn out useful to quite a wide 
range of authors.

> Er..ok you say something weird I don't get:

It is probably just how I said it...

>
> """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."""
>
> Does this mean that if I had:
>
> inferedSubClass(uncle, brother)
> subClass(uncle, complementOf(brother)
>
> and your other axioms, the ontology wouldn't be inconsistent? (That
> introduces non-monotonicity, which is a different game...)

I intended that this *would be* inconsistent - no knowledge-base containing 
subClass(uncle, complementOf(brother)) can entail subClass(uncle, brother), 
so the inferedSubClass constraint is violated. Any ontology where 
intersection(uncle, complementOf(brother)) is not empty violates what I 
intended by inferedSubClass.

I probably shouldn't have spoken in terms of consistency. Buggy or broken was 
more what I had in mind. But I don't think we can assume that an ontology 
that violates the entailments intended by the ontology author is safe to use, 
ontologically (as in things may not mean what we think they mean), just as we 
can't assume that an ontology that is inconsistent is safe to use logically.

Is that any clearer?

>
> Cheers,
> Bijan.

Matthew

Received on Wednesday, 27 February 2008 23:10:04 UTC