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 >=:

(=> (Nonnegative-Integer ?X) (>= ?X 0))

(=> (Non-Negative-Integer@Kif-Extensions ?X) (>= ?X 0))

(=> (Nth-Domain@Frame-Ontology ?Relation ?N ?Type)
    (Forall 
        (?Tuple)
        (=> (Member@Ol-User%Kif-Sets ?Tuple ?Relation)
            (And (>= (Length@Ol-User%Kif-Lists ?Tuple) ?N)
                 (Instance-Of@Frame-Ontology 
                     (Nth@Ol-User%Kif-Lists ?Tuple ?N)
                     ?Type)))))

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

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


Equivalence Axioms mentioning >=:

(<=> (Non-Negative-Integer@Kif-Extensions ?X)
     (And (Integer ?X) (>= ?X 0)))

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

(<=> (Minimum-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)))

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

(<=> (Quanterm@Ol-User%Kif-Meta ?X)
     (Or (Exists (?T ?P)
                 (And (Term@Ol-User%Kif-Meta ?T)
                      (Sentence@Ol-User%Kif-Meta ?P)
                      (= ?X (Listof 'The ?T ?P))))
         (Exists (?T ?P)
                 (And (Term@Ol-User%Kif-Meta ?T)
                      (Sentence@Ol-User%Kif-Meta ?P)
                      (= ?X (Listof 'Setofall ?T ?P))))
         (Exists (?Vlist ?P)
                 (And (List@Ol-User%Kif-Lists ?Vlist)
                      (Sentence@Ol-User%Kif-Meta ?P)
                      (>= (Length@Ol-User%Kif-Lists ?Vlist) 1)
                      (=> (Item@Ol-User%Kif-Lists ?V ?Vlistp)
                          (Indvar@Ol-User%Kif-Meta ?V))
                      (= ?X (Listof 'Kappa ?Vlistp ?P))))
         (Exists (?Vlist ?Sv ?P)
                 (And (List@Ol-User%Kif-Lists ?Vlist)
                      (Seqvar@Ol-User%Kif-Meta ?Sv)
                      (Sentence@Ol-User%Kif-Meta ?P)
                      (=> (Item@Ol-User%Kif-Lists ?V ?Vlist)
                          (Indvar@Ol-User%Kif-Meta ?V))
                      (= ?X
                         (Listof 'Kappa
                                 (Append@Ol-User%Kif-Lists ?Vlist
                                         (Listof ?Sv))
                                 ?P))))
         (Exists (?Vlist ?T)
                 (And (List@Ol-User%Kif-Lists ?Vlist)
                      (Term@Ol-User%Kif-Meta ?T)
                      (>= (Length@Ol-User%Kif-Lists ?Vlist) 1)
                      (=> (Item@Ol-User%Kif-Lists ?V ?Vlistp)
                          (Indvar@Ol-User%Kif-Meta ?V))
                      (= ?X (Listof 'Lambda ?Vlistp ?T))))
         (Exists (?Vlist ?Sv ?T)
                 (And (List@Ol-User%Kif-Lists ?Vlist)
                      (Seqvar@Ol-User%Kif-Meta ?Sv)
                      (Sentence@Ol-User%Kif-Meta ?T)
                      (=> (Item@Ol-User%Kif-Lists ?V ?Vlist)
                          (Indvar@Ol-User%Kif-Meta ?V))
                      (= ?X
                         (Listof 'Lambda
                                 (Append@Ol-User%Kif-Lists ?Vlist
                                         (Listof ?Sv))
                                 ?T))))))


Axioms mentioning >=:

(>= (Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation) 1)