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, ab
  • an inequality statement, ab

where a, bI individual names, CC a concept expression, and RR a role.