+ is the addition 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. First, the sum of two quantities is only defined when the quantities are comparable -- having the same dimension -- and the sum has the same dimension. Second, the sum of two constant quantities is the sum of their magnitudes. However, the magnitude of a quantity is relative to a unit in which it is requested. Therefore, the sum of two quantities x and y is another quantity z such that for all units of measure of comparable dimension, the magnitude of z in such a unit is the sum of the magnitude of x and y in that unit.The + function is further specialized when applied to different kinds of quantities, such as constant-quantities, function-quantities, and vector-quantities. These specialization are defined as polymorphic extensions in the corresponding theories.
In the case of CONSTANT-QUANTITY, + is more strongly defined. The sum of the magnitudes of two compatible-quantities is equal to the magnitude of the sum of the quantities, for all units of measure.
(=> (And (Constant-Quantity ?X) (Constant-Quantity ?Y))
(<=> (+ ?X ?Y ?Z)
(And (Constant-Quantity ?Z)
(Forall (?Unit)
(=> (Unit-Of-Measure ?Unit)
(= (+ (Magnitude ?X ?Unit)
(Magnitude ?Y ?Unit))
(Magnitude ?Z ?Unit)))))))
(=> (And (Physical-Quantity ?X) (Physical-Quantity ?Y) (+ ?X ?Y ?Z))
(And (Physical-Quantity ?Z)
(Compatible-Quantities ?X ?Y)
(Compatible-Quantities ?X ?Z)))