Is-unique-if

Is-unique-if defines a key for a class. Keys are for uniquely identifying an individual. The open-world assumption does not imply that some things (e.g. concepts, instances) are disjoint if they are named differently. The uniqueness of two individuals can be inferred from rules. If two named instances of the class coincide on values for each of key properties, then these two individuals are the same. With more complex construction, two individuals can be reasoned to be different from each other.

OWL 1 does not provide a means to define keys. The OWL 2 construct HasKey allows keys to be defined for a given class.

Examples

Those examples show how to define and use keys in CNL.

Example: Tom and Mark can be theoretically the same individual.
Tom is a man.
Mark is a man.
Example: Tom and Mark are reasoned to be different individuals.
Every X that is a man is-unique-if X has-id equal-to something.
Every man has-id one (some integer value).
Mark is a man and has-id equal-to 11.
Tom is a man and has-id equal-to 12.
Example: Tom and Mark are reasoned to be the same individuals.
Every X that is a man is-unique-if X has-id equal-to something.
Mark is a man and has-id equal-to 11.
Tom is a man and has-id equal-to 11.