Function +

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

Slots on this function:

Documentation:

For Tensors in general:

Addition is defined for two tensors of equal spatial dimension, and results in a tensor of the same spatial dimension. The usual restrictions for physical-quantities also apply.

For Vectors:

When defined, the addition of vector-quantities can be decomposed into additions of scalar components. This decomposition corresponds to choosing an arbitrary basis, mapping the vector-quantities to components in that basis, and summing appropriate components.

For Dyads,

When defined, the addition of dyads can be decomposed into additions of scalar components. This decomposition corresponds to choosing an arbitrary basis, mapping the dyads to components in that basis, and summing appropriate components.

Axioms:

(Forall (?Physdim ?Spatdim)
        (Abelian-Group (Dyad-Of-Dimensions ?Physdim ?Spatdim)
                       +
                       (The-Zero-Dyad-Of-Type ?Spatdim ?Physdim)))

(=> (And (Dyad ?X) (Dyad ?Y))
    (=> (+ ?X ?Y ?Z)
        (And (Dyad ?Z)
             (Forall (?B ?I ?J)
                     (=> (And (Orthonormal-Basis ?B)
                              (= (Spatial.Dimension ?X)
                                 (Basis.Dimension ?B))
                              (Positive-Integer ?I)
                              (Positive-Integer ?J)
                              (=< ?I (Spatial.Dimension ?X))
                              (=< ?J (Spatial.Dimension ?X)))
                         (= (Dyad-Component ?Z ?I ?J ?B)
                            (+ (Dyad-Component ?X ?I ?J ?B)
                               (Dyad-Component ?Y ?I ?J ?B))))))))

(Forall (?Physdim ?Spatdim)
        (Abelian-Group (Vector-Quantities-Of-Dimensions ?Physdim
                                                        ?Spatdim)
                       +
                       (The-Zero-Vector-Of-Type ?Spatdim ?Physdim)))

(=> (And (Vector-Quantity ?X) (Vector-Quantity ?Y))
    (=> (+ ?X ?Y ?Z)
        (And (Vector-Quantity ?Z)
             (Forall (?B ?I)
                     (=> (And (Orthonormal-Basis ?B)
                              (= (Spatial.Dimension ?X)
                                 (Basis.Dimension ?B))
                              (Positive-Integer ?I)
                              (=< ?I (Spatial.Dimension ?X)))
                         (= (Vector-Component ?Z ?I ?B)
                            (+ (Vector-Component ?X ?I ?B)
                               (Vector-Component ?Y ?I ?B))))))))

(=> (And (Tensor-Quantity ?X) (Tensor-Quantity ?Y) (+ ?X ?Y ?Z))
    (And (Tensor-Quantity ?Z)
         (= (Spatial.Dimension ?X) (Spatial.Dimension ?Y))
         (= (Spatial.Dimension ?X) (Spatial.Dimension ?Z))))