DTV 1.0b2 FTF Avatar
  1. OMG Issue

DTV — CLIF Logic Errors

  • Key: DTV-16
  • Legacy Issue Number: 16690
  • Status: closed  
  • Source: General Electric ( Mark Linehan)
  • Summary:

    Various logical errors in the CLIF axioms need correction:

    1. In clause E.1.2, the axiom under concept "sequence is of concept" reads:

    (forall ((member thing) (s sequence))
    (exists ((c concept))
    (iff ("sequence is of concept" s c)
    (if "member participates in sequence" member s)
    ("concept corresponds to instance" c member)))))

    and should probably read:

    (forall (s sequence)
    (exists (c concept)
    (iff ("sequence is of concept" s c)
    (forall (member thing)
    (if ("member participates in sequence" member s)
    ("concept corresponds to instance" c
    2. Several of the verb concepts in clause E.1.5 range specifically over "unique sequences". In several cases, the axioms are not written to match the concept types that the roles range over.

  • Reported: DTV 1.0b1 — Thu, 17 Nov 2011 05:00 GMT
  • Disposition: Resolved — DTV 1.0b2
  • Disposition Summary:

    The formulations in (1) are logically equivalent, but neither is the definition of ‘sequence is of concept’. Issue 17225 points out that the structure of the definitions in Annex D is generally poor. The text that resolves this issue is included in that resolution.

    Revised Text:

    Disposition: Merged with Issue 17225

  • Updated: Fri, 6 Mar 2015 20:58 GMT