DTV — Corollaries to Axiom D.4 in 8.2.3 are misstated

In clause 8.2.3 (p.54), the first corollary to axiom D.4 is stated in mathematical English:
If t1 and t2 are time intervals such that t1 starts t2, then D(t1 starts t2 complementing t3) = D(t2) ­
D(t1).
But "t1 starts t2 complementing t3" is a proposition, which does not have a duration. The intent is:
If t1, t2 and t3 are time intervals such that t1 starts t2 complementing t3, then D(t3) = D(t2) ­ D(t1).

There is a further requirement, namely that time interval t2 is "finite" (which does not seem to be a concept in clause 8). 'Time interval has particular duration' cannot always be satisfied. So it appears that the term 'finite time interval' must be defined: A time interval that has a duration.

The CLIF formulation of this corollary is also incorrect. It should read:
(forall ((t1 "time interval") (t2 "time interval") (t3 "time interval"))
(if
(and
(exists ((d duration))
("time interval has duration" t2 d)
("time interval1 starts time interval2 complementing
time interval3" t1 t2 t3))
(= ("duration of" t3)
(- ("duration of" t2) ("duration of" t1))) ))

If the concept 'finite time interval' is added, then this can be simplified:
(forall ((t1 "finite time interval") (t2 "finite time interval")
(t3 "finite time interval"))
(if
("time interval1 starts time interval2 complementing
time interval3" t1 t2 t3)
(= ("duration of" t3)
(- ("duration of" t2) ("duration of" t1))) ))

The second Corollary has the same problem. It reads:
If t1 and t2 are time intervals such that t1 finishes t2, then D(t1 finishes t2 complementing t3) = D(t2) ­
D(t1).
It should read:
If t1, t2 and t3 are time intervals such that t1 finishes t2 complementing t3, then D(t3) = D(t2) ­ D(t1).

The CLIF formulation of the second corollary is also incorrect. It should read:
(forall ((t1 "finite time interval") (t2 "finite time interval")
(t3 "finite time interval"))
(if
("time interval1 finishes time interval2 complementing
time interval3" t1 t2 t3)
(= ("duration of" t3)
(- ("duration of" t2) ("duration of" t1))) ))

In both cases, the existence of time interval t3 is the subject of a different axiom. So it suffices to say, for any three time intervals that are related in a certain way, their durations are related in a certain way.

The remaining issue is that Clause 8.2 does not define the CLIF function for the SBVR attributive construct 'duration of'. Axiom D.2 suddenly introduces the notation "duration of" as a function. The intent is that the fact type 'time interval has duration' introduces both a CLIF predicate "time interval has duration" AND a CLIF function, which can be defined axiomatically as:
(forall ((t "finite time interval") (d duration))
(iff ("time interval has duration" t d)
(= ("duration of" t) d) ))
This declaration should be added to the entry for the fact type that introduces the "attributive role" 'duration'.

Note also that construction of a CLIF function from an SBVR attributive role pattern only behaves as expected when the role is played by a unique thing for each possible value of the function argument. If it is possible that the role is empty or multivalued for a valid argument, the CLIF function would have to be described as returning a set. So this construct does not follow some general pattern. It must be appropriately declared in each case. In this case, the supporting axiom:
Necessity: Each time interval has at most one particular duration.
should be stated, and then the above function axiom completes the model.

The technical changes to the CLIF formulations are accepted in principle. The formulation of the Corollaries is corrected. The CLIF function "duration of" is defined. The definition of 'particular duration' and the related axioms are modified. The style of the CLIF formulations, however, follows Issue 17225.
The FTF disagrees that the concept “finite time interval” is needed. It is the intent of the DTV that all time intervals are “finite” – they have a beginning and an end. But the open world assumption may apply: Time intervals can be “indefinite” in the sense that we don’t know the beginning or the end. This is clarified in the text.
There are other errors in the formulation of the axioms in 8.2.3 with respect to the “duration of” role, and they are also corrected.