Function QUANTITY.DIMENSION

• Defined in theory: Physical-quantities
• Source code: physical-quantities.lisp

Slots on this function:

Documentation:

A quantity has a unique physical-dimension. This function maps quantities to physical-dimensions. It is total for all physical quantities (as stated in the definition of physical-quantity).

Instance-Of: Function

Arity: 2

Domain: Physical-quantity

Range: Physical-dimension

Other Related Axioms:

(Inherited-Facet-Value Slot-Cardinality
                       Physical-Quantity
                       Quantity.Dimension
                       1)

(=> (Physical-Quantity ?X)
    (Value-Cardinality ?X Quantity.Dimension 1))

(=> (Quantity.Dimension $X $Y) (Physical-Dimension $Y))

(=> (Quantity.Dimension $X $Y) (Physical-Quantity $X))

(<=> (Compatible-Quantities ?X ?Y)
     (And (Physical-Quantity ?X)
          (Physical-Quantity ?Y)
          (= (Quantity.Dimension ?X) (Quantity.Dimension ?Y))))

(<= (Quantity.Dimension $X Identity-Dimension)
    (Dimensionless-Quantity $X))

(<=> (Dimensionless-Quantity ?X)
     (And (Constant-Quantity ?X)
          (= (Quantity.Dimension ?X) Identity-Dimension)))

(=> (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-Quantity ?X) (Recip ?X ?Y))
    (And (Physical-Quantity ?Y)
         (= (Quantity.Dimension ?Y)
            (Expt (Quantity.Dimension ?X) -1))))

(=> (And (Physical-Quantity ?X) (Real-Number ?R) (Expt ?X ?R ?Z))
    (And (Physical-Quantity ?Z)
         (= (Quantity.Dimension ?Z)
            (Expt (Quantity.Dimension ?X) ?R))))

(= (Quantity.Dimension Identity-Unit) Identity-Dimension)

(Instance-Of (Setofall ?Dim
                       (Exists (?Unit)
                               (And (Member ?Unit
                                            (Base-Units ?System))
                                    (= ?Dim
                                       (Quantity.Dimension ?Unit)))))
             Orthogonal-Dimension-Set)

(Orthogonal-Dimension-Set 
    (Setofall ?Dim
              (Exists (?Unit)
                      (And (Member ?Unit (Base-Units ?System))
                           (= ?Dim (Quantity.Dimension ?Unit))))))

(=> (Instance-Of ?Unit ?System)
    (= (Standard-Unit ?System (Quantity.Dimension ?Unit)) ?Unit))

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

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

(<- (Magnitude-In-System-Of-Units ?Q ?System)
    (Magnitude ?Q (Standard-Unit ?System (Quantity.Dimension ?Q))))

Notes:

• Example: (= (quantity.dimension (height fred)) length-dimension)