Class SCALAR-QUANTITY


Slots on this class:

Documentation:
A scalar-quantity is a constant quantity whose magnitude is a real number. An important property of scalar-quantities is that they form a field with respect to the addition and multiplication (with proper subclass restrictions). The class of scalar-quantities forms a partial order with the less-than relation <, since < is a relation-extended-to-quantities and < is defined over the reals. The < relation is not a total order over the class of scalar-quantity
since elements from some subclasses such as length quantities are incomparable to elements from other subclasses such as mass quantities.
Instance-Of: Class
Subclass-Of: Constant-quantity
Has-Instance: Identity-scalar
Partial-Order: <
Range-Of: The-zero-scalar-for-dimension
Superclass-Of: Real-number

Equivalence Axioms:

(<=> (Scalar-Quantity ?Q)
     (And (Constant-Quantity ?Q)
          (Forall (?U)
                  (=> (And (Unit-Of-Measure ?U)
                           (Compatible-Quantities ?U ?Q))
                      (Real-Number (Magnitude ?Q ?U))))))


Axioms:

(Forall (?U)
        (=> (And (Unit-Of-Measure ?U) (Compatible-Quantities ?U ?Q))
            (Real-Number (Magnitude ?Q ?U))))

(Constant-Quantity ?Q)


Other Related Axioms:

(<=> (Scalar-Quantity ?Q)
     (And (Constant-Quantity ?Q)
          (Forall (?U)
                  (=> (And (Unit-Of-Measure ?U)
                           (Compatible-Quantities ?U ?Q))
                      (Real-Number (Magnitude ?Q ?U))))))

(Identity-Element-For Identity-Scalar * Scalar-Quantity)

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

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

(=> (And (Scalar-Quantity ?X) (Recip ?X ?Y))
    (And (Scalar-Quantity ?Y)
         (Forall (?Dim)
                 (=> (/= ?X (The-Zero-Scalar-For-Dimension ?Dim))
                     (= (* ?X ?Y) Identity-Scalar)))))

(=> (And (Scalar-Quantity ?X) (Real-Number ?R) (Expt ?X ?R ?Z))
    (And (Scalar-Quantity ?Z)
         (=> (= ?R 0) (= ?Z 1))
         (Forall (?U)
                 (=> (Unit-Of-Measure ?U)
                     (= (Expt (Magnitude ?X ?U) ?R)
                        (Magnitude ?Z (Expt ?U ?R)))))))

(<- (Scalar-Quantities-Of-Dimension ?Dimension)
    (If (Physical-Dimension ?Dimension)
        (Kappa (?Q)
               (And (Scalar-Quantity ?Q)
                    (= (Quantity.Dimension ?Q) ?Dimension)))))

(=> (The-Zero-Scalar-For-Dimension $X $Y) (Scalar-Quantity $Y))

(=> (= (The-Zero-Scalar-For-Dimension ?Dimension) ?Zero-Scalar)
    (Scalar-Quantity ?Zero-Scalar))