We frequently have situations where we want to make an assertion combining parthood and cardinality. Here, cardinality pertains to the number of instances.
Section 5.3 of the OWL2 primer has an example of a cardinality restriction,
Individual: John Types: hasChild max 4 Parent
This is saying that John has at most 4 children that are parents.
A more natural biological example of a cardinality restriction is stating something like:
Class: Hand SubClassOf: hasPart exactly 5 Finger
i.e. every hand has exactly 5 fingers. Remember we are following the open world assumption here – we are not saying that our ontology has to list all 5 fingers. We are stating that in our model of the world, any instance of a hand h entails the existence of 5 distinct finger instances f1…f5, each of which is related to that hand, i.e. fn part-of h. Furthermore there are no other finger instances not in the set f1..5 that are part of h.
The precise set-theoretic semantics and provided in the OWL2 Direct Semantics specification.
This cardinality axiom seems like a perfectly natural, reasonable, and useful thing to add to an ontology (avoiding for now discussions about “canonical hands” and “variant hands”, for example in cases like polydactyly; let’s just assume we are describing “canonical anatomy”, whatever that is).
And in fact there are various ontologies in OBO that do this kind of thing.
However, there is a trap here. If you try and run a reasoner such as HermiT you will get a frankly perplexing and unhelpful error such as this.
An error occurred during reasoning: Non-simple property 'BFO_0000051' or its inverse appears in the cardinality restriction 'BFO_0000051 exactly 5 UBERON_1234567
If you have a background in computer science and you have some time to spare you can go and look at section 11 of the OWL specification (global restrictions on axioms in OWL2 DL) to see what the magical special laws you must adhere to when writing OWL ontologies that conform to the DL profile, but it’s not particularly helpful to understand:
- why you aren’t allowed to write this kind of thing, and
- what the solution is.
Why can’t I say that?
A full explanation is outside the scope of this article, but the basic problem arises when combining transitive properties such as part-of with cardinality constraints. It makes the ontology fall outside the “DL” profile, which means that reasoners such as HermiT can’t use it, so rather ignore it HermiT will complain and refuse to reason.
Well I want to say that anyway, what happens if I do?
You may choose to assert the axiom anyway – after all, it may feel useful for documentation purposes, and people can ignore it if they don’t want it, right? That seems OK to me, but I don’t make the rules.
Even if you don’t intend to stray outside DL, an insidious problem arises here: many OBO ontologies use Elk as their reasoner, and Elk will happily ignore these DL violations (as well as anything it can’t reason over, outside it’s variant of the EL++ profile). This in itself is totally fine – its inferences are sound/correct, they just might not be complete. However, we have a problem if an ontology includes these DL violations, and the relevant portion of that ontology is extracted and then used as part of another ontology with a DL reasoner such as HermiT that fails fast when presented with these axioms. In most pipelines, if an ontology can’t be reasoned, it can’t be released, and everything is gummed up until an OWL expert can be summoned to diagnose and fix the problem. Things get worse if an ontology that is an N-th order import has a DL violation, as it may require waiting for all imports in the chain to be re-released. Not good!
Every now and then this happens with an OBO ontology and things get gummed up, and people naturally ask the usual questions, why did this happen, why can’t I say this perfectly reasonable thing, how do I fix this, hence this article.
How do we stop people from saying that?
Previously we didn’t have a good system for stopping people from making these assertions in their ontologies, and the assertions would leak via imports and imports of imports, and gum things up.
Now we have the wonderful robot tool and the relatively new validate-profile command, which can be run like this:
robot validate-profile --profile DL \
--input my-ontology.owl \
--output validation.txt
This will ensure that the ontology is in the DL profile. If it isn’t, this will fail, so you can add this to your Makefile in order to fail fast and avoid poisoning downstream ontologies.
This check will soon be integrated into the standard ODK setup.
OK, so how do I fix these?
So you have inadvertently strayed outside the DL profile and your ontology is full of has-parts with cardinality constraints – you didn’t mean it! You were only alerted when a poor downstream ontology imported your axioms and tried to use a DL reasoner. So what do you do?
In all honesty, my advice to you is ditch that axiom. Toss it in the bin. Can it. Flush that axiom down the toilet. Go on. It won’t be missed. It was already being ignored. I guarantee it wasn’t doing any real work for you (here work == entailments). And I guarantee your users won’t miss it.
A piece of advice often given to aspiring writers is to kill your darlings, i.e. get rid of your most precious and especially self-indulgent passages for the greater good of your literary work. The same applies here. Most complex OWL axioms are self-indulgences.
Even if you think you have a really good use case for having these axioms, such as representing stoichiometry of protein complexes or reaction participants, the chances are that OWL is actually a bad framework for the kind of inference you need, and you should be using some kind of closed-world reasoning system, e.g. one based on datalog.
OK, so maybe you don’t believe me, and you really want to say something that approximates your parts-with-numbers. Well, you can certainly weaken your cardinality restriction to an existential restriction (provided the minimum cardinality is above zero; for maxCardinality of zero you can use a ComplementOf). So in the anatomical example we could say
Class: Hand SubClassOf: hasPart some Finger
This is still perfectly sound – it is not as complete as your previous statement, but does that matter? What entailments were you expecting from the cardinality axiom. If this is intended more for humans, you can simply annotate your axiom with a comment indicating that humans typically have 5 fingers.
OK, so you still find this unsatisfactory. You really want to include a cardinality assertion, dammit! Fine, you can have one, but you won’t like it. We reluctantly added a sub-property of has-part to RO called ‘has component’:
In all honesty the definition for this relation is not so great. Picking holes in it is not so hard. It exists purely to get around this somewhat ridiculous constraint, and for you to be able to express your precious cardinality constraint, like this:
Class: Hand SubClassOf: hasComponent exactly 5 Finger
So how does this get around the constraint? Simple: hasComponent is not declared transitive. (recall that transitivity is not inferred down a property hierarchy). Also it is a different relation (a subproperty) from has-part, so you might not get the inferences you expect. For example, this does NOT prevent me from making an instance of hand that has as parts 6 distinct fingers – it only applies to the more specific relation, which we have not asserted, and is not inferred.
You can make an argument that this is worse than useless – it gives no useful entailments, and it confuses people to boot. I am responsible for creating this relation, and I have used it in ontologies like Uberon, but I now think this was a mistake.
Other approaches
There are other approaches. For a fixed set of cardinalities you could create subproperties, e.g. has-1-part-of, has-2-parts-of, etc. But these would still be less expressive than you would like, and would confuse people.
A pattern that does work in certain cases such as providing logical definitions for things like cells by number of nuclei is to use the EL-shunt pattern (to be covered in a future article) and make characteristic classes in an ontology like PATO.
While this still isn’t as expressive, it allows you to use proxies for cardinality in logical definitions (which do actual work for you), and shunt off the cardinality reasoning to a smaller ontology — where really it’s actually fine to just assert the hierarchy.
But this doesn’t work in all cases. There is no point making characteristics/qualities if they are not reused. It would be silly to do this with the hand example (e.g. making a has5fingers quality).
Isn’t this all a bit annoying?
Yes, it is. In my mind we should be free to state whatever axioms we need for our own use cases, expressivity be damned. I should be able to go outside DL, in fact to use anything from FOL or even beyond. We should not be condemned to live in fear of stepping outside of decidability (which sounds like something you want, but in practice is not useful). There are plenty of good strategies for employing a hybrid reasoning strategy, and in any case, we never use all of DL for most large OBO ontologies anyway.
But we have the technology we do, and we have to live with it for now.
TL;DR
- don’t mix parthood and cardinality
- you probably won’t miss that cardinality restriction anyway
- no really, you won’t
- use robot to check your profiles
Monkeying around with OWL 