DTV — DTV Issue: inaccurate formulation of definitions in CLIF

Specification: Date Time Vocabulary
Version: beta-1
Title: inaccurate formulation of definitions in CLIF
Source: Michael Gruninger <gruninger@mie.utoronto.ca>

Summary:
In the OMG Date Time Vocabulary, all of the axioms use relativized quantifiers,
even for defined relations. For example,

(forall ((t1 "time interval") (t2 "time interval"))
(iff ("time interval1 equals time interval2" t1 t2)
(and ("time interval1 is part of time interval2" t1 t2)
("time interval1 is part of time interval2" t2 t1))))

This sentence is equivalent to

(forall (t1 t2)
(if (and ("time interval" t1) ("time interval" t2))
(iff ("time interval1 equals time interval2" t1 t2)
(and ("time interval1 is part of time interval2" t1 t2)
("time interval1 is part of time interval2" t2 t1))))

It seems to me that what is really wanted is
(forall (t1 t2)
(iff ("time interval1 equals time interval2" t1 t2)
(and ("time interval" t1) ("time interval" t2)
("time interval1 is part of time interval2" t1 t2)
("time interval1 is part of time interval2" t2 t1))))

Recommendation:
For all of the predicates that are type-specific, change all the definitions to use simple quantifiers and make the typing of the arguments part of the equivalent condition. This would also eliminate the need for many uses of relativized quantifiers in other Date Time Vocabulary axioms.

The FTF concurs with the proposed change of practice for specification of definitions in CLIF.
The resolution of this issue addresses a number of changes to the CLIF specification elements, including other changes in the style of formulations and the repair of various CLIF syntax errors, including those noted in Issue 16690.

These corrections are applied in a single "bulk" change in order to ensure that that the CLIF logic matches the SBVR design and because it is easiest to work in one language at a time.