Function +

Instance-Of@Frame-Ontology: Function@Ol-User%Kif-Relations, Relation@Ol-User%Kif-Relations, Set@Ol-User%Kif-Sets
Arity@Frame-Ontology: 3
If $tau_1$, ..., $tau_n$ are numerical constants, then the term {tt (+ $tau_1 ... tau_n$)} denotes the sum $tau$ of the numbers
corresponding to those constants.

and also:

+ denotes a time range ?time-range-2 whose length is longer

that ?time-range-1 by a duration ?duration.

A difference between two time points ?time-point-1 and ?time-point-2 is a

duration ?duration.

Implication Axioms for +:

(=> (And (Duration@Simple-Time ?Duration-1)
         (Duration@Simple-Time ?Duration-2))
    (=> (= (+ ?Duration-1 ?Duration-2) ?Duration-3)
        (Duration@Simple-Time ?Duration-3)))

(=> (+ ?Time-Range-1 ?Duration)
    (=> (And (Time-Point@Simple-Time ?Time-Range-1)
             (Duration@Simple-Time ?Duration))
        (=> (= (+ ?Time-Point-1 ?Duration) ?Time-Point-2)
            (And (Time-Point@Simple-Time ?Time-Point-1)
                 (Duration@Simple-Time ?Duration)
                 (Time-Point@Simple-Time ?Time-Point-2)))))

(=> (+ ?Time-Range-1 ?Duration)
    (=> (And (Time-Range@Simple-Time ?Time-Range-1)
             (Duration@Simple-Time ?Duration))
        (<=> (= (+ ?Time-Range-1 ?Duration) ?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))))))

Axioms for +:

(Undefined@Ol-User%Kif-Extensions (Arity@Frame-Ontology +))

Implication Axioms mentioning +:

(=> (Time-Range@Simple-Time ?Time-Range)
    (Equals@Simple-Time (+ (Start-Time-Of@Simple-Time ?Time-Range)
               (Duration-Of@Simple-Time ?Time-Range))
            (End-Time-Of@Simple-Time ?Time-Range)))