Function +

Slots on this function:

+ defines the specialization of the quantity addition operator + for scalar-quantities. The operator enforces the restriction that the quantities be compatible. The operator is defined in terms of the number addition operator + and the magnitudes of quantities for a particular unit. Scalar-Quantities of a common dimension form an abelian group with respect to this operator and the zero-scalar of the same physical dimension.


(Forall (?D)
        (=> (Physical-Dimension ?D)
            (Abelian-Group (Scalar-Quantities-Of-Dimension ?D)
                           (The-Zero-Scalar-For-Dimension ?D))))

(=> (And (Scalar-Quantity ?X) (Scalar-Quantity ?Y))
    (<=> (+ ?X ?Y ?Z)
         (And (Scalar-Quantity ?Z)
              (Forall (?U)
                      (=> (And (Unit-Of-Measure ?U)
                               (Compatible-Quantities ?X ?U))
                          (= (+ (Magnitude ?X ?U) (Magnitude ?Y ?U))
                             (Magnitude ?Z ?U)))))))