Function +

• Defined in theory: Scalar-quantities
• Source code: scalar-quantities.lisp
• Also defined in: Kif-numbers, Physical-quantities, Unary-scalar-functions, Basic-matrix-algebra, Tensor-quantities

Slots on this function:

Documentation:

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

Axioms:

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