Class UNIT-OF-MEASURE


Slots on this class:

Documentation:
A unit-of-measure is a constant-quantity that serves as a standard of measurement for some dimension. For example, the meter is a unit-of-measure for the length-dimension, as is the inch. Square-feet is a unit for length*length quantities. Units-of-measure can be defined as primitives or can be defined as products of units or units raised to real exponents.

There is no intrisic property of a unit that makes it primitive or fundamental; rather, a system-of-units defines a set of orthogonal dimensions and assigns units for each. Therefore, there is no distinguished class for fundamental unit of measure.

The magnitude of a unit-of-measure is always a positive real number, using any comparable unit. Units are not scales, which have reference origins and can have negative values. Units are like distances between points on scales.

Any composition of units and reals using the * and expt functions is also a unit-of-measure. For example, the quantity 'three meters' is denoted by the expression (* 3 meter). There is an identity-unit that forms and abelian-group with the * operator over units of measure. That means * is commutative and associative for units. It is also commutative for multiplying units and other constant-quantities. This is important for factoring out units from expressions containing tensors or functions.

Instance-Of: Class
Subclass-Of: Constant-quantity
Has-Instance: Identity-unit

Implication Axioms:

(=> (And (Unit-Of-Measure ?A) (Constant-Quantity ?B))
    (= (* ?A ?B) (* ?B ?A)))

(=> (And (Unit-Of-Measure ?A) (Real-Number ?B))
    (Unit-Of-Measure (Expt ?A ?B)))


Equivalence Axioms:

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


Axioms:

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

(Constant-Quantity ?U)

(Abelian-Group Unit-Of-Measure * Identity-Unit)


Other Related Axioms:

(Nth-Domain Magnitude 2 Unit-Of-Measure)

(Forall (?Q ?Unit ?Mag)
        (=> (And (Constant-Quantity ?Q)
                 (Unit-Of-Measure ?Unit)
                 (Dimensionless-Quantity ?Mag)
                 (Defined (* ?Mag ?Q)))
            (= (Magnitude (* ?Mag ?Q) ?Unit)
               (* ?Mag (Magnitude ?Q ?Unit)))))

(=> (= (Magnitude ?Q ?Unit) ?Mag) (Unit-Of-Measure ?Unit))

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

(Forall (@Args)
        (<=> (And (Holds ?R @Args)
                  (=> (Item ?Q (Listof @Args))
                      (Constant-Quantity ?Q)))
             (Forall (?Unit ?Q)
                     (=> (And (Unit-Of-Measure ?Unit)
                              (=> (Item ?Q (Listof @Args))
                                  (Compatible-Quantities ?Q ?Unit)))
                         (Member (Map (Lambda (?Q)
                                              (Magnitude ?Q ?Unit))
                                      (Listof @Args))
                                 ?R)))))

(<=> (Relation-Extended-To-Quantities ?R)
     (And (Relation ?R)
          (Forall (@Args)
                  (<=> (And (Holds ?R @Args)
                            (=> (Item ?Q (Listof @Args))
                                (Constant-Quantity ?Q)))
                       (Forall (?Unit ?Q)
                               (=> (And (Unit-Of-Measure ?Unit)
                                        (=> (Item ?Q (Listof @Args))
                                            (Compatible-Quantities 
                                                ?Q
                                                ?Unit)))
                                   (Member (Map (Lambda 
                                                    (?Q)
                                                    (Magnitude ?Q
                                                               ?Unit))
                                                (Listof @Args))
                                           ?R)))))))

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

(=> (And (Unit-Of-Measure ?A) (Constant-Quantity ?B))
    (= (* ?A ?B) (* ?B ?A)))

(=> (And (Unit-Of-Measure ?A) (Real-Number ?B))
    (Unit-Of-Measure (Expt ?A ?B)))

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

(<= (Subclass-Of $X Unit-Of-Measure) (System-Of-Units $X))

(Inherited-Slot-Value System-Of-Units Subclass-Of Unit-Of-Measure)

(<=> (System-Of-Units ?System)
     (And (Class ?System)
          (Subclass-Of ?System Unit-Of-Measure)
          (=> (Instance-Of ?Unit ?System)
              (= (Standard-Unit ?System (Quantity.Dimension ?Unit))
                 ?Unit))
          (Value-Cardinality ?System Base-Units 1)
          (=> (Member ?Unit (Base-Units ?System))
              (Instance-Of ?Unit ?System))
          (Orthogonal-Dimension-Set 
              (Setofall ?Dim
                        (Exists (?Unit)
                                (And (Member ?Unit
                                             (Base-Units ?System))
                                     (= ?Dim
                                        (Quantity.Dimension ?Unit))))))))

(=> (= (Base-Units ?System-Of-Units) ?Set-Of-Units)
    (=> (Member ?Unit ?Set-Of-Units) (Unit-Of-Measure ?Unit)))

(Nth-Domain Standard-Unit 3 Unit-Of-Measure)

(=> (= (Standard-Unit ?System-Of-Units ?Dimension) ?Unit)
    (Unit-Of-Measure ?Unit))