Re: post-conditions in OWL files

I did something along the lines of the external test suite for a BioPAX
prototype. See
http://biopaxwiki.org/cgi-bin/moin.cgi/Validator_BioPAX_Access_via_SPARQL
-Alan

On Thu, Feb 28, 2008 at 8:09 AM, Matthew Pocock <matthew.pocock@ncl.ac.uk>
wrote:

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