I’ve been cleaning up the amino acids ontology by removing unwanted axioms, rationalising the annotations and, importantly for this exercise, adding lots of new defined classes. The latest amino acids ontology is available. In short, the amino acids ontology takes each of the 20 amino acids used in biology and describes them according to their polarity, hydrophobicity, charge, size and the aliphatic/aromatic nature of the side chain.
I’ve put in lots of defined classes such as aliphatic amino acid; positively charged amino acid, polar amino acid, hydrophilic amino acid all being defined as equivalent to the appropriate restriction. These are straiht-forward and have the expected effect. The class:
Class: SmallAminoAcid EquivlentTo: AminoAcid that hasSize some Small
After reasoning (hasSize is functional), this has thamino acids Cysteine, Aspartate, Glutamate, Asparagine, Proline and Valine as subclasses. a similar class for Tiny amino acids has Alanine, glycine, Serine and Threonine.
If we then create a class such as:
Class: SmallPolarAminoAcid equivalentTo: SmallAminoAcid and PolarAminoAcid
after reasoning we have the amino acids Cysteine and Asparagine, underneath, and, of course, this is a kind of SmallAminoAcid and a kind of PolarAminoAcid.
this is all straight-forward. Some more interesting things happen because of the covering axiom in the ontology. For AminoAcid, we have the following axiom:
Class: AminoAcid EquivalentTo: [in amino-acid.owl] Alanine or Cysteine or Aspartate or Glutamate or Phenylalanine or glycine or Histidine or Isoleucine or Lysine or Leucine or Methionine or Asparagine or Proline or Glutamine or Arginine or Serine or Threonine or Valine or Tryptophan or Tyrosine
This is a closure axiom that says that if an individual is an amino acid, then it has to be one of these amino acids. It also says that is an individual is a member of one of these classes, then it must be an amino acid. the useful semantics here is that we’re saying the only amino acids that can exist are these 20 amino acids that are used in biology. Chemically this covering axiom is not justified, but it is biologically true (as long as we ignore modified amino acids). As we now “know” all the amino acids, we start inferring more things. For instance:
LargeAromaticAminoAcid and AromaticAminoAcid both have Phenylalanine, Histidine, tryptophan, and Tyrosine as subclasses. In our locally closed world, we can now infer that these two classes are equivalent (they have the same extents). This reveals a small biochemical truth — being aromatic means being large and aromatic; all the aromatic side chains in biological amino acids make the side chains large.
Now, if we make a class such as:
Class: SmallPositiveAminoAcid EquivalentTo: SmallAminoAcid and PositiveChargedAminoAcid
it becomes unsatisfiable. With the covering axiom we “know” all the amino acids. We know this intersection will be empty in this version of the world and so it is unsatisfiable as there are no amino acids that are both small and positively charged — and the autmated reasoners has told us so.
We have lots of examples of inferred quivalence in this ontology. LargeChargedAminoAcid and LargePositiveChargedAminoAcid are the same thing; if an amino acid is large and charged, then it is positively charged. similarly, SmallPolarAminoAcid and SmallPolarAliphaticAminoAcid (Cysteinine and Asparagine) – an amino acid cannot be small and aromatic, so has to be aliphatic. Finally, we see that the classes SmallChargedPolarAminoAcid, SmallChargedAminoAcid and NegativeChargedAminoAcid are all equivlaent and subsume Aspartate, glutamate and Tyrosine, and are equivalent. Again, some small biochemical truth is here – to be small an amino acid has to be aliphatic. If an amino acid is small and charged then it is negatively charged and so on.
all these inferences about equivalence and unsatisfiability are driven by the covering axiom. Ontologically this is not right, this is not an exhaustic list of all amino acids, but just the biologically “interesting” ones. If the covering axiom was undesireable, it is useful in development to see which classes are redundant and unsatisfiable. the unsatisfiable classes can have no instances, but it may be useful to this for teaching reasons (a trivial example, but it makes the point well enough) as one can show why the classes are unsatisfiable because this “closed” world has no instances of the types described and this reflects some simple biochemistry. It may be that biochemically, one may wish to highlight the equivalence of many forms and how the chemistry drives such a view. The covering axiom reveals this and the equivalences and unsatisfiability would not be revealed without the covering axiom.