Issue 16690: CLIF Logic Errors (date-time-ftf)
Source: International Business Machines (Mr. Mark H. Linehan, mlinehan(at)us.ibm.com)
Nature: Uncategorized Issue
Severity: 
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        
            member))))))
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.


Resolution: 
Revised Text: 
Actions taken:
November 17, 2011: recewived issue
Discussion: 

End of Annotations:=====
MG Issue No:  16690 
Title:	CLIF Logic Errors
Source:
Mark H. Linehan . IBM . mlinehan@us.ibm.com

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        
            member))))))
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.