* 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.
and also:
* is the multiplication operator for physical-quantities. The * function is defined for numbers as part of KIF specification (in the kif-numbers ontology). Here it is extended polymorphically to operate on physical quantities. The main difference between quantities and ordinary numbers is the notion of dimension and unit. The dimension of the product of two quantities is the analogous product of their dimensions (the * function is also extended to dimensions). For example, the product of two length quantities is a quantity of dimension 'length * length'.The relationship between the magnitudes of two quantities and their product cannot be stated completely in this ontology. It depends on the whether the magnitudes are scalars or higher-order tensors. The * function is further specialized when applied to these different kinds of quantities in the ontologies for scalar-quantities and vector-quantities. It must be commutative and associative, however, in order to allow factoring of magnitudes and units.
The function * is also a commutative and associative operator for specifying products of PHYSICAL-DIMENSIONS. Together with the identity-dimension, * forms an abelian group over physical-dimensions.
and also:
Defines the specialization of the multiplication operator * for unary-scalar-function-quantitys. It is defined for the cases where both its arguments are USFs, and also when the first is a scalar and the second is a USF.
and also:
If $tau_1$, ..., $tau_n$ denote numbers, then the term {tt (* $tau_1 ldots tau_n$)} denotes the product of those numbers.
(=> (And (Physical-Dimension ?D1)
(Physical-Dimension ?D2)
(* ?D1 ?D2 ?D3))
(Physical-Dimension ?D3))
(=> (And (Physical-Quantity ?X) (Physical-Quantity ?Y) (* ?X ?Y ?Z))
(And (Physical-Quantity ?Z)
(= (Quantity.Dimension ?Z)
(* (Quantity.Dimension ?X) (Quantity.Dimension ?Y)))))
(=> (And (Physical-Dimension ?D1)
(Physical-Dimension ?D2)
(* ?D1 ?D2 ?D3))
(Physical-Dimension ?D3))
(=> (And (Physical-Quantity ?X) (Physical-Quantity ?Y) (* ?X ?Y ?Z))
(And (Physical-Quantity ?Z)
(= (Quantity.Dimension ?Z)
(* (Quantity.Dimension ?X) (Quantity.Dimension ?Y)))))
(=> (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)))))))
(=> (And (Unary-Scalar-Function-Quantity ?X)
(Unary-Scalar-Function-Quantity ?Y)
(* ?X ?Y ?Z))
(Unary-Scalar-Function-Quantity ?Z))
(Undefined (Arity *))
(Undefined (Arity *))
(Undefined (Arity *))
(Undefined (Arity *))
(Distributes * + Physical-Quantity)
(Undefined (Arity *))
(Undefined (Arity *))
(Undefined (Arity *))
(Undefined (Arity *))
(Distributes * + Physical-Quantity)
(Abelian-Group
(Kappa (?X)
(And (Scalar-Quantity ?X)
(Forall (?Dim)
(=> (Physical-Dimension ?Dim)
(/= (The-Zero-Scalar-For-Dimension ?Dim)
?X)))))
*
1)
(=> (And (Unary-Scalar-Function-Quantity ?X)
(Unary-Scalar-Function-Quantity ?Y)
(* ?X ?Y ?Z))
(Unary-Scalar-Function-Quantity ?Z))
(Forall (?F ?G ?R)
(=> (And (Unary-Scalar-Function-Quantity ?F)
(Unary-Scalar-Function-Quantity ?G)
(Real-Number ?R))
(And (= (Deriv (+ ?F ?G)) (+ (Deriv ?F) (Deriv ?G)))
(= (Deriv (* ?F ?G))
(+ (* (Deriv ?F) ?G) (* ?F (Deriv ?G))))
(= (Deriv (Expt ?F ?R))
(* ?R (Expt (Deriv ?F) (1- ?R)))))))