**Definition (ABox).** An ABox A is a finite collection of axioms of the form *C*(*a*), *R*(*a*, *b*), where *a* and *b* are individual names, *C* is a concept, and *R* is a role. An individual assertion can be

- a concept assertion,
*C*(*a*) - a role assertion,
*R*(*a*,*b*), or a negated role assertion, ¬*R*(*a*,*b*) - an equality statement,
*a*≈*b* - an inequality statement,
*a*≉*b*

where *a*, *b* ∈ **I** individual names, *C* ∈ **C** a concept expression, and *R* ∈ **R** a role.