DTV 1.0b2 FTF Avatar
  1. OMG Issue

DTV — D0 Should be Quantified

Open Closed All
  • Key: DTV-15
  • Legacy Issue Number: 16689
  • Status: closed  
  • Source: General Electric ( Mark Linehan)
  • Summary:

    Clause 7.2.2 has several CLIF axioms that reference 'D0' but fail to quantify that variable. They should each existentially quantify 'D0'.
  • Reported: DTV 1.0b1 — Thu, 17 Nov 2011 05:00 GMT
  • Disposition: Resolved — DTV 1.0b2
  • Disposition Summary:

    In 8.2.2, D0 is declared to be an individual concept – a logical constant – under Axiom V.4. The problem is that there is no CLIF rendition of this axiom, and there needs to be a theorem that D0 is unique.
    In resolving this issue, the FTF noted that the CLIF operators (+, –, *) must be defined between durations, because they are not the same as the operators for numbers. And the closure axiom does not follow from the definition.
  • Updated: Fri, 6 Mar 2015 20:58 GMT