Description Logics; mandatory participation

Question

I have a UML conceptual diagram; and I want to express it as DL ontology. UML classes are captured as DL concepts, where associations are captured by means of roles. One important perspective is multiplicities among UML classes. A to-one multiplicity (0..* - 0..1) is captured by a functional object property, and to make the one (0..1) side mandatory, i.e. (0..* - 1) references talk about mandatory participation implying a maximum and minimum multiplicity of 1 on the to-one side.

Here is the reference

An association A between classes C1 and C2 is formalized in DL by means of a role A on which we enforce the assertions

To express the multiplicity ml..mu on the participation of instances of C2 for each given instance of C1, we use the assertion

I just cannot understand how the mandatory participation of C2 in the assertion is expressed by an assertion on C1, how is the last assertion read?

Answer 1

Using A a as a property name is a bit unusual, so I'm going to use p instead. The UML diagram doesn't express the direction of the property either, which makes the rest of the discussion a bit confused. Some information can be gleaned from the axioms you've provided, though.

If the UML is designed to express:

1. Instances of C₁ are related by p to at least n_l and and most n_u instances of C₂.
2. At least m_l and and most m_u instances of C₁ are related by p to each instance of C₂.

then you could use the DL axioms:

C₁ ⊑ ≥n_l p.C₂
C₁ ⊑ ≤n_u p.C₂
C₂ ⊑ ≥m_l p^-1.C₁
C₂ ⊑ ≥m_u p^-1.C₁

Those say that if x is a C₁ (C₂) then x is related to the appropriate number of C₂ (C₁) instances by p (p^-1). Now, since the relationship as expressed in UML will only relate instances of the two classes, i.e., no other types of instances will be related by property p, then it's more likely that you would declare the domain and range of p as C₁ and C₂, respectively, with:

∃p ⊑ C₁
∃p^-1 ⊑ C₂

and then use a simpler version of the axioms above:

C₁ ⊑ ≥n_l p
C₁ ⊑ ≤n_u p
C₂ ⊑ ≥m_l p^-1
C₂ ⊑ ≥m_u p^-1

To answer the very specific question:

just cannot understand how the mandatory participation of C2 in the assertion is expressed by an assertion on C1, how is the last assertion read?

The notation in the last axiom in the question is unusual, and I'm not sure exactly what's supposed to be. I'm not sure what the little circumflexes are suppose to be. It looks like:

C₁ ⊑ ∃ p

though. If that's what it is, it's read as

C₁ is a subclass of ∃ p

which means that that

If x is an instance of C₁ then x is an instance of ∃ p

which means that

If x is an instance of C₁ then x is an instance of the class of things that have at least value for p (i.e., there is at least one y such that p(x,y)).

In first-order logic, you could express it as:

∀x.(C₁(x) → ∃y.p(x,y))