Augmentation of Function +

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

Instance-Of: Function, Relation, Set

Arity: 3

Documentation:

+ 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.

and also:

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.

Implication Axioms for +:

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

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

(=> (+ ?Time-Range-1 ?Duration)
    (=> (And (Time-Range ?Time-Range-1) (Duration ?Duration))
        (<=> (= (+ ?Time-Range-1 ?Duration) ?Time-Range-2)
             (And (= (Start-Time-Of ?Time-Range-1)
                     (Start-Time-Of ?Time-Range-2))
                  (= (+ (End-Time-Of ?Time-Range-1) ?Duration)
                     (End-Time-Of ?Time-Range-2))))))

Axioms for +:

(Undefined (Arity +))

Implication Axioms mentioning +:

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