Relation =<

Instance-Of@Frame-Ontology: Binary-Relation@Ol-User%Kif-Relations, Relation@Ol-User%Kif-Relations, Set@Ol-User%Kif-Sets
Arity@Frame-Ontology: 2

Equivalence Axioms for =<:

(<=> (=< ?X ?Y) (Or (= ?X ?Y) (< ?X ?Y)))


Implication Axioms mentioning =<:

(=> (= (Projection@Frame-Ontology ?Relation ?Column)
       ?Projection-Relation)
    (=< ?Column (Arity@Frame-Ontology ?Relation)))

(=> (Maximum-Value-Cardinality@Frame-Ontology ?Instance
                               ?Binary-Relation
                               ?N)
    (=< (Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation)
        ?N))

(=> (Has-At-Most@Ol-User%Slot-Constraint-Sugar ?Instance
                 ?Binary-Relation
                 ?N)
    (=< (Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation)
        ?N))

(=> (= (Minutes-Of@Simple-Time ?Time-Point) ?Minutes)
    (=< ?Minutes 59))

(=> (= (Minutes-Of@Simple-Time ?Time-Point) ?Minutes)
    (=< 0 ?Minutes))


Equivalence Axioms mentioning =<:

(<=> (Projection@Frame-Ontology ?Relation ?Column)
     (And (Defined@Ol-User%Kif-Extensions 
              (Arity@Frame-Ontology ?Relation))
          (Positive-Integer@Ol-User%Kif-Extensions ?Column)
          (=< ?Column (Arity@Frame-Ontology ?Relation))
          (Class@Frame-Ontology ?Projection-Relation)
          (Forall (?Projection-Instance)
                  (<=> (Instance-Of@Frame-Ontology 
                           ?Instance
                           ?Projection-Relation)
                       (Exists (?Tuple)
                               (And (Member@Ol-User%Kif-Sets ?Tuple
                                            ?Relation)
                                    (= (Nth@Ol-User%Kif-Lists ?Tuple
                                            ?Column)
                                       ?Instance)))))))

(<=> (Maximum-Value-Cardinality@Frame-Ontology ?Instance
                                ?Binary-Relation
                                ?N)
     (And (Binary-Relation@Ol-User%Kif-Relations ?Binary-Relation)
          (Nonnegative-Integer ?N)
          (=< (Value-Cardinality@Frame-Ontology ?Instance
                                 ?Binary-Relation)
              ?N)))

(<=> (Maximum-Slot-Cardinality@Frame-Ontology ?Domain-Class
                               ?Relation
                               ?N)
     (=> (Instance-Of@Frame-Ontology ?Instance ?Domain-Class)
         (=< (Value-Cardinality@Frame-Ontology ?Instance ?Relation)
             ?N)))

(<=> (Has-At-Most@Ol-User%Slot-Constraint-Sugar ?Instance
                  ?Binary-Relation
                  ?N)
     (And (Binary-Relation@Ol-User%Kif-Relations ?Binary-Relation)
          (Natural ?N)
          (=< (Value-Cardinality@Frame-Ontology ?Instance
                                 ?Binary-Relation)
              ?N)))

(<=> (Integer-Range@Ranges ?Class)
     (And (Class@Frame-Ontology ?Class)
          (Subclass-Of@Frame-Ontology ?Class Integer)
          (Value-Cardinality@Frame-Ontology ?Class
                             I-Lower-Bound@Ranges
                             1)
          (Value-Cardinality@Frame-Ontology ?Class
                             I-Upper-Bound@Ranges
                             1)
          (Forall (?I)
                  (=> (Instance-Of@Frame-Ontology ?I ?Class)
                      (And (=< (I-Lower-Bound@Ranges ?Class) ?I)
                           (=< ?I (I-Upper-Bound@Ranges ?Class)))))))