Trivially satisfiable classes

Summary

We are used to having an automated reasoner tell us when we’ve described an impossibility in our ontologies. In this case, it is possible to change the axioms to “repair” these impossibilities. Now there are various ways that we can write axioms that somehow describe an impossibility (http://ontogenesis.knowledgeblog.org/1329) (or an impossibility that will only be apparent in a certain situation) that will not be detected by a reasoner: for example, if I declare two classes to be disjoint, then a common instance is an impossibility, but no reasoner will tell me this unless prompted explicitly – even though, if I was to instantiate the conjunction of those 2 disjoint classes, I would make my ontology inconsistent. In a similar way, when using the universal quantifier (the only in Manchester OWL syntax) one can say the only filler for this property, should it exist, is something that is impossible according to my ontology – but as we’ve not said that there is an instance of this filler it won’t really show. We’ve called this trivial satisfiability (10.1007/978-3-540-30202-5_5) – what has been said is trivially satisfiable according to the semantics of the language, but there can be horrid consequences later on. In this kblog we explain this notion and illustrate with some axioms.

Authors

Robert Stevens
Bio-health Informatics Group
School of Computer Science
University of Manchester
Oxford Road
Manchester
United Kingdom
M13 9PL
robert.stevens@Manchester.ac.uk

the main bit

If we write an axiom such as

Cell SubClassOf hasPart only CellularComponent

we’re saying that if an instance of Cell were to have a part, it could only be a CellularComponent; we’re not saying one is actually there (or exists) in this relationship to the left-hand-side. That is the job of the existential quantifier or the some of Manchester OWL Syntax); e.g.:

Cell SubClassOf hasPart some CellularComponent

A problem may arise when using a universal quantification with an “impossible” filler. For instance, if we wanted to say that the filler in our example was the intersection of CellularComponent and SmallMolecule and that these were disjoint:

Cell SubClassOf hasPart only (CellularComponent and SmallMolecule)

DisjointClasses(CellularComponent, SmallMolecule)

and ran the reasoner, we’d find that all of this was satisfiable and our ontology coherent (http://ontogenesis.knowledgeblog.org/1329). This is in spite of the fact we’ve said that nothing can be an instance of both CellularComponent and SmallMolecule, and that we’d need to have such an instance if we ever wanted to have a part of a Cell.

We’ve said the only filler for this restriction on Cell would be the intersection of CellularComponent and SmallMolecule. However, as we’ve not said that there exists one of these instances of CellularComponent and SmallMolecule in this situation, everything’s OK – it is trivially satisfiable (10.1007/978-3-540-30202-5_5). That is, we’ve not actually said anything wrong according to the semantics of the language and the axioms of the ontology. It’s trivial because it’s not a very strong statement – it’s trivial to satisfy the stated constraint.

As soon as I add, to the above two axioms, something like

Cell SubClassOf hasPart some Nucleus

(even without adding that Nucleus is a kind of CellularComponent) and run a reasoner, it all goes wrong. Here, we’ve said that Cell can only have parts that are from the intersection of CellularComponent and SmallMolecule. In our example, Nucleus is tested to see if it can come from CellularComponent and SmallMolecule and finds that the class is impossible – so an unsatisfiability occurs, i.e., the class Cell is unsatisfiable w.r.t. our three axioms.

Whenever one has a universal class expression P only C without a matching existential P some D that is either asserted or inferred, then the universal P only C is trivially satisfiable, namely by elements that don’t have any P-successors. Only when an existential restriction also demands some P-successors there can be problems.

Of course this isn’t usually a problem if attention is paid to the constraints imposed by an ontology’s axiomatisation to what can act as a filler to an axiom. There are, however, some patterns that may make this kind of slip more probable. Take, for instance, the pattern (10.1186/1471-2105-11-441):

ContinuantClass SubClassOf has-Function some (Function and realized-by only Process)

which can occur all over the place when describing functions of gene products and the biological processes in which they participate. We can use the existential on hasFunction, as the gene product always has the function (for arguments sake), but we don’t really want to say that there exists a biological process in which that function is realised; that is, not all proteins with a given function do actually participate in the processes appropriate to that gene product’s function. This kind of use of the universal also occurs where there are hypothetical outcomes that don’t actually exist – speculations about diagnosis outcomes and the like.

Let’s take an example from the field of gene products. As above, I can say

FunctionX SubClassOf regulates only MetabolicProcess

as well as

FunctionY SubClassOf (FunctionX and (regulates only CellCycleProcess))

DisjointClasses(MetabolicProcess, CellCycleProcess)

and the reasoner will say that this is OK (i.e., this ontology is consistent and has no unsatisfiable classes) and it is – despite the fact that no FunctionY can ever have any regulatory function: if a FunctionY would ever be regulates related to something, then this would have to be a

• CellCycleProcess (because it is regulated by a FunctionY, and also a
• MetabolicProcess (because it is regulated by a FunctionX because this is a superclass of FunctionY),

but nothing can be both a CellCycleProcess and a MetabolicProcess. Hence nothing can be a FunctionY and regulates some Thing.

Hence all will remain fine until I add something that says there are instances of FunctionY – either via an existential restriction on FunctionY for some cell cycle process or some individual that asserts a fact about FunctionY regulating something. Of course, this may never happen – the patterns may dictate no existentials and individuals may never be generated. The ontology would remain coherent, but have potential glitches.

There’s another nice example of trivial satisfiability in

Person and hasPet only (Unicorn and hasColour some Pink)

is satisfied by a Person with no pets at all. the axiom is saying that if the person had a pet, then it would have to be a pink unicorn, but seeing as it hasn’t, it still complies with the axiom. In the same way, the author is a member of the class of people that only have children that are Nobel prize winners (the author has no children).

Should I be worried?

Sort of: the issue is that there is no way of checking the validity of trivially satisfiable axioms and classes without saying something exists. One either has to bite the bullet and say something that is a little untrue (such as all gene products participate in a process) or one has to have some testing regime that takes the trivaly satisfiable axiom and automatically generates the existential equivalent, runs the reasoner, generates a report, etc. without the existential axiom ever actually being in the ontology.

It may be that this sort of axiom is a risk you’re prepared to take, but it should be done knowingly.

Bibliography