If a property is declared to be inverse-functional, then the object of a property statement uniquely determines the subject (some individual). More formally, if we state that P is an owl:InverseFunctionalProperty, then this asserts that a value y can only be the value of P for a single instance x, i.e. there cannot be two distinct instances x1 and x2 such that both pairs (x1,y) and (x2,y) are instances of P.
Syntactically, an inverse-functional property axiom is specified by declaring
the property to be an instance of the built-in OWL class owl:InverseFunctionalProperty,
which is a subclass of the OWL class
A typical example of an inverse-functional property:
This example states that for each object of
statements (some human) one should be able to uniquely identify a subject (some
woman). Inverse-functional properties resemble the notion of a key in databases.
Because in OWL Full datatype properties are a subclass of object properties, an inverse-functional property can be defined for datatype properties. In OWL DL object properties and datatype properties are disjoint, so an inverse-functional property cannot be defined for datatype properties.
One difference with functional properties is that for inverse-functional properties no additional object-property or datatype-property axiom is required: inverse-functional properties are by definition object properties.
specify global cardinality constraints. That is, no matter which class the
property is applied to, the cardinality constraints must hold. This is different
from the cardinality constraints contained in property
restrictions. The latter are class descriptions and are only enforced on the
property when applied to that class.