Closing Down the Open World: Covering Axioms and Closure Axioms

OWL has an open world assumption. This means that just because we don’t say something doesn’t mean it isn’t true. For example, we have an ontology of amino acids (latest amino acid ontology) and we have subclassses for all 20 naturally occurring amino acids. Unless we tell the ontology and the automated reasoner that there can be no others, it is assumed that there can be. Similarly, in the pizza tutorial, I can say that a Margherita pizza has both a tomato topping and a mozzarella topping, but unless I explicitly say that there are no other toppings, it is assumed there may be other toppings that I just haven’t mentioned.

sometimes we wish to close down descriptions of entities, so that we’re saying “There are these things and there are no others”; we want to have a locally “closed world”. This can be done when describing the children of a particular class – there are these subclasses and no others; similarly, we often wish to say instances of a class have relationships via a particulaar property to specified entities, but have no othre relationship via this particvular property.

The covering axiom

If we wanted to make a simple description of sex as being either male or female, we would have the following sets of axioms:

Class: Sex
SubClassOf: (Male or Female)

Class: Female
SubClassOf:
        Sex

Class: Male
SubClassOf :
        Sex

DisjointClasses: Female, Male

Here we are saying the following:

1. There are the classes Sex, Female and Male;
2. Each and every instance of Female is also an instance of Sex (the subclass axiom);
3. Each and every instance of Male is also an instance of Sex; (the subclass axiom);
4. An instance of Sex, cannot be both an instance of Male and an instance of Female (the disjointness axiom);
5. All instances of Sex must be instances of the union class (Male or Female); that is, they must be one of either male or female, and with the disjointnesss axiom we know that they must be one or the other, but not both.

Making Sex a subclass of the disjunction (Male or Female) is saying that Sex must be one of these two classes. The subclass axioms from Male and Female to Sex says that, for instance, each and every instance of Male must also be an instance of sex. It now works the other way around too: Sex SubClassOf: Male or Female says that Sex must be one of these two classes as well. Sex is now “covered” by Male or Female.

If we say Sex EquivlaentTo: (Female or Male), we’re saying that being a member of the class (Female or Male) is enough to recognise an instance of either Male or Female as being a member of the class Sex. Equivalence has implications both ways; the subclass axiom says that Male implies Sex, but not that Sex implies Male. With equivalence, however, saying Sex EquivalentTo: Male or Female says that the implication now goes from Sex to Male and Female; saying something is of the class Sex is enough to know that it is one of Male or Female. In this case, the subclass axiom from Male and Female to Sex is not needed.

Both the equivalence axiom and the subclass axiom with the disjunction serve to close or cover the kinds of children the class in question can have. It must be remembered, however, that with the subclass covering axiom, all the subsumption axioms are required, as well as the covering axiom itself.

the amino acids ontology (initial blog) (latest amino acid ontology)drammatically shows the effects of a covering axiom. By saying that amino acid is “covered by” the 20 amino acids used in biological systems (a dodgey statement), then the reasoner knows that these are the only amino acids. If we create a class such as one defining “Large amino acid” as any amino acid that is large in size and also one defining “Aromatic amino acid”, as any amino acid with an aromatic side-chain we find that they are inferred to be equivalent. Both have the same inferred subclasses and as we know we know all the amino acids, these two classes can thus be inferred to be equivalent. Without the covering axiom, it may be that there is an aromatic side chain that isn’t large, so such a conclusion could not be drawn.

In addition, A covering axiom can cause classes to become unsatisfiable. We can similarly define “Small aromatic amino acid” as any amino acid that is both small in size and has an aromatic side-chain. There are no amino acids with this combination of attributes that are “covered” by the “amino acid” class and, as we know all the amino acids, we know that this class can have no members in our model of the world, so it is unsatisfiable.

The closure axiom

WE use anonymous subclass axioms as restrictions upon classes. We might say, for example that:

Class: Cell
        SubClassOf: hasPart some PlasmaMembrane

This says that each and every instance of Cell must have at least one hasPart property between it and an instance of the class PlasmaMembrane. OWL’s open world assumption means that there may be other hasPart properties from cell to other entities, even if we haven’t explicitly said that there are other parts of this kind of cell. To say that the only hasPart property held by instances of cell is to “PlasmaMembrane+ instances, we’d have to add cell hasPart only PlasmaMembrane. While the existential quantifier used in hasPart some PlasmaMembrane means that there must be at least one hasPart property to an instance of PlasmaMembrane, but there may be other hasPart properties to other types of entity, the universal quantifier (only) means that PlasmaMembrane is the only kind of entity that can exist at the end of a hasPart property held by an instance of Cell. (However, without the existential version, we don’t know that there is such a property held by an instance of Cell.)

If cell has many hasPart properties to other kinds of instance (such as hasPart some Mitochondrion; hasPart some EndoPlasmicReticulum; hasPart some Nucleus), we can easily say that these are the only entities to which cell can hold a hasPart property. The closure axiom hasPart only (PlasmaMembrane or Mitochondrion or EndoPlasmicReticulum or Nucleus), means that if an instance of Cell holds a +hasPart+property with any instance, then it must be an instance of this disjunction.

Summary

The open world is a useful modelling tool. In biology we don’t want to assume that just because we’ve not said it that it isn’t true. Our knowledge is incomplete — saying a red blood cell participates in oxygen transport and then assuming it participates in no other biological processes would be doing red blood cells a dis-service. However, we do wish to locally close down our descriptions and the covering axiom and the closure axiom are two commonly used ways of doing this.