Issue 17225: DTV Issue: inaccurate formulation of definitions in CLIF (date-time-ftf)
Source: NIST (Mr. Edward J. Barkmeyer, edbark(at)nist.gov)
Nature: Uncategorized Issue
Severity: 
Summary: 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.
Resolution: 
Revised Text: 
Actions taken:
March 12, 2012: received issue
Discussion: 

End of Annotations:=====

m: Ed Barkmeyer <edbark@nist.gov>
To: issues@omg.org
Subject: 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.