Relation <

Instance-Of@Frame-Ontology:
Binary-Relation@Ol-User%Kif-Relations, Binary-Relation@Ol-User%Kif-Relations, Relation@Ol-User%Kif-Relations, Relation@Ol-User%Kif-Relations, Relation@Ol-User%Kif-Relations ...
Inverse@Ol-User%Kif-Relations: >
Arity@Frame-Ontology: 2
Documentation@Ol%Frame-Ontology:
The sentence {tt (< $tau_1$ $tau_2$)} is true if and only if the number denoted by $tau_1$ is less than the number denoted by $tau_2$.

and also:

a time point ?time-point-1 preceeds a time point ?time-point-2.

Implication Axioms for <:

(=> (< ?Time-Point-1 ?Time-Point-2)
    (=> (And (Time-Point@Simple-Time ?Time-Point-1)
             (Time-Point@Simple-Time ?Time-Point-2))
        (<=> (< ?Time-Point-1 ?Time-Point-2)
             (Or (< (Year-Of@Simple-Time ?Time-Point-1)
                    (Year-Of@Simple-Time ?Time-Point-2))
                 (And (= (Year-Of@Simple-Time ?Time-Point-1)
                         (Year-Of@Simple-Time ?Time-Point-2))
                      (Or (< (Month-Of@Simple-Time ?Time-Point-1)
                             (Month-Of@Simple-Time ?Time-Point-2))
                          (And (= (Month-Of@Simple-Time ?Time-Point-1)
                                  (Month-Of@Simple-Time ?Time-Point-2))
                               (Or (< (Day-Of@Simple-Time ?Time-Point-1)
                                      (Day-Of@Simple-Time ?Time-Point-2))
                                   (And (= (Day-Of@Simple-Time ?Time-Point-1)
                                           (Day-Of@Simple-Time ?Time-Point-2))
                                        (Or (< (Hour-Of@Simple-Time ?Time-Point-1)
                                               (Hour-Of@Simple-Time ?Time-Point-2))
                                            (And (= (Hour-Of@Simple-Time ?Time-Point-1)
                                                    (Hour-Of@Simple-Time ?Time-Point-2))
                                                 (Or (< (Minute-Of@Simple-Time ?Time-Point-1)
                                                        (Minute-Of@Simple-Time ?Time-Point-2))
                                                     (And (= (Minute-Of@Simple-Time ?Time-Point-1)
                                                             (Minute-Of@Simple-Time ?Time-Point-2))
                                                          (< (Second-Of@Simple-Time ?Time-Point-1)
                                                             (Second-Of@Simple-Time ?Time-Point-2)))))))))))))))


Implication Axioms mentioning <:

(=> (Negative ?X) (< ?X 0))

(=> (> ?Time-Point-1 ?Time-Point-2)
    (=> (And (Time-Point@Simple-Time ?Time-Point-1)
             (Time-Point@Simple-Time ?Time-Point-2))
        (<=> (> ?Time-Point-1 ?Time-Point-2)
             (< ?Time-Point-2 ?Time-Point-1))))

(=> (During@Simple-Time ?Time-Range-1 ?Time-Range-2)
    (< (End-Time-Of@Simple-Time ?Time-Range-1)
       (End-Time-Of@Simple-Time ?Time-Range-2)))

(=> (Overlaps@Simple-Time ?Time-Range-1 ?Time-Range-2)
    (< (End-Time-Of@Simple-Time ?Time-Range-1)
       (End-Time-Of@Simple-Time ?Time-Range-2)))

(=> (Overlaps@Simple-Time ?Time-Range-1 ?Time-Range-2)
    (< (Start-Time-Of@Simple-Time ?Time-Range-2)
       (End-Time-Of@Simple-Time ?Time-Range-1)))


Equivalence Axioms mentioning <:

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

(<=> (Before@Simple-Time ?Time-Range-1 ?Time-Range-2)
     (< (End-Time-Of@Simple-Time ?Time-Range-1)
        (Start-Time-Of@Simple-Time ?Time-Range-2)))

(<=> (After@Simple-Time ?Time-Range-1 ?Time-Range-2)
     (< (End-Time-Of@Simple-Time ?Time-Range-2)
        (Start-Time-Of@Simple-Time ?Time-Range-1)))

(<=> (During@Simple-Time ?Time-Range-1 ?Time-Range-2)
     (And (> (Start-Time-Of@Simple-Time ?Time-Range-1)
             (Start-Time-Of@Simple-Time ?Time-Range-2))
          (< (End-Time-Of@Simple-Time ?Time-Range-1)
             (End-Time-Of@Simple-Time ?Time-Range-2))))

(<=> (Overlaps@Simple-Time ?Time-Range-1 ?Time-Range-2)
     (And (< (Start-Time-Of@Simple-Time ?Time-Range-1)
             (Start-Time-Of@Simple-Time ?Time-Range-2))
          (< (Start-Time-Of@Simple-Time ?Time-Range-2)
             (End-Time-Of@Simple-Time ?Time-Range-1))
          (< (End-Time-Of@Simple-Time ?Time-Range-1)
             (End-Time-Of@Simple-Time ?Time-Range-2))))