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 multiplication operator * for scalar-quantities. The operator enforces the relationship between the physical-dimensions of the operands and the product. The operator is defined in terms of the number multiplication operator * and the magnitudes of quantities for a particular unit. Scalar-Quantities excluding all the zero-scalars form an abelian group with respect to this operator and the identity-scalar <1>. This operator distributes over the + operator for scalar-quantities,
providing a field behavior with restrictions.

Axioms:

(Abelian-Group 
    (Kappa (?X)
           (And (Scalar-Quantity ?X)
                (Forall (?Dim)
                        (=> (Physical-Dimension ?Dim)
                            (/= (The-Zero-Scalar-For-Dimension ?Dim)
                                ?X)))))
    *
    1)

(=> (And (Scalar-Quantity ?X) (Scalar-Quantity ?Y))
    (<=> (* ?X ?Y ?Z)
         (And (Scalar-Quantity ?Z)
              (Forall (?U ?U1 ?U2)
                      (=> (And (Unit-Of-Measure ?U)
                               (Compatible-Quantities ?X ?U)
                               (Unit-Of-Measure ?U1)
                               (Compatible-Quantities ?Y ?U1)
                               (Unit-Of-Measure ?U1)
                               (= (Quantity.Dimension ?U2)
                                  (* (Quantity.Dimension ?U)
                                     (Quantity.Dimension ?U1))))
                          (= (* (Magnitude ?X ?U1)
                                (Magnitude ?Y ?U2))
                             (Magnitude ?Z ?U)))))))