Function +

• Defined in ontology: Kif-numbers
• Source pathname: /tmp_mnt/vol/q/htw/cms/ontolingua/examples/kif/../../all-ontologies/kif/kif-numbers.lisp
• Also defined in: Physical-quantities, Basic-matrix-algebra, Unary-scalar-functions, Simple-time, Scalar-quantities, Tensor-quantities

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

Arity@Frame-Ontology: 3

Documentation@Ol%Frame-Ontology:

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)
                        ?Duration)
                     (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)))