;;; -*- Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*- 

;;; Physical Quantities Ontology 
;;; (c) 1993 Greg Olsen and Thomas Gruber 

(in-package "ONTOLINGUA-USER") 

(define-theory physical-quantities (frame-ontology abstract-algebra) 

"In engineering analysis, physical quantities such as the length of a beam 
or the velocity of a body are routinely modeled by variables in equations 
with numbers as values.  While human engineers can interpret these numbers as 
physical quantities by inferring dimension and units from context, the 
representation of quantities as numbers leaves implicit other relevant 
information about physical quantities in engineering models, such as physical 
dimension and unit of measure.  Furthermore, there are many classes of models 
where the magnitude of a physical quantity is not a simple real number - a 
vector or higher-order tensor for instance.  Our goal here is to extend 
standard mathematics to include unit and dimension semantics. 

In this theory, we attempt to define the basic concepts associated 
with physical quantities.  A quantity is a hypothetically measurable 
amount of something.  We refer to those things whose amounts are 
described by physical-quantities as physical-dimensions (following the 
terminology used in most introductory Physics texts).  Time, length, 
mass, and energy are examples of physical-dimensions.  Comparability 
is inherently tied to the concept of quantities.  Quantities are 
described in terms of reference quantities called units-of-measure.  A 
meter is an example of an unit-of-measure for quantities of the length 

The physical-quantities theory defines the basic vocabulary for 
describing physical quantities in a general form, making explicit the 
relationships between magnitudes of various orders, units of measure 
and physical dimensions.  It defines the general class 
physical-quantity and a set of algebraic operators that are total over 
all physical quantities.  Specializations of the physical-quantity 
class and the operators are defined in other theories (which use 
this theory). 

The theory also describes specific language for physical units such as 
meters, inches, and pounds, and physical dimensions such as length, 
time, and mass.  The theory provides representational vocabulary to 
compose units and dimensions from basis sets and to describe the basic 
relationships between units and physical dimensions.  This theory 
helps support the consistent use of units in expressions relating 
physical quantities, and it also supports conversion of units needed 
in calculations.") 

(in-theory 'physical-quantities) 

;;;  Physical Quantities  

(define-class PHYSICAL-QUANTITY (?x) 

  "A physical-quantity is a measure of some quantifiable aspect of the 
modeled world, such as 'the earth's diameter' (a constant length) and 
'the stress in a loaded deformable solid' (a measure of stress, which 
is a function of three spatial coordinates).  The first type is called 
constant-quantity and the second type is called function-quantity. 
All physical quantities are either constant-quantities or 
function-quantities.  Although the name and definition of this concept 
is inspired from physics, physical quantities need not be material. 
For example, amounts of money are physical quantities.  In fact, 
all real numbers and numeric-valued tensors are special cases of physical  
quantities.  In engineering textbooks, quantities are often called variables. 

   Physical quantities are distinguished from purely numeric entities 
like a real numbers by their physical dimensions.  A 
physical-dimension is a property that distinguishes types of 
quantities.  Every physical-quantity has exactly one associated 
physical-dimension.  In physics, we talk about dimensions such as 
length, time, and velocity; again, nonphysical dimensions such as 
currency are also possible.  The dimension of purely numeric entities 
is the identity-dimension. 

   The 'value' of a physical-quantity depends on its type.  The value of 
a constant-quantity is dependent on a unit-of-measure.  Physical 
quantities of the identity-dimension (dimensionless quantities) are 
just numbers or tensors to start with.  Physical quantities of the 
type function-quantity are functions that map quantities to other 
quantities (e.g., time-dependent quantities are function-quantities). 
See the definitions of these other classes and functions for detail." 

   ;; every physical quantity has a dimension 
  :def (defined (quantity.dimension ?x)) 

   ;; physical quantities are either quantities or quantity functions 
  :axiom-def (and (exhaustive-subclass-partition 

           ("We define a general class of quantities in order to  
             support a generic set of operators.  Most of the semantics  
             of these operators are not given here.  Specializations  
             of quantity will define how each operator works over 
             their domains (i.e., subclasses of quantity)."))) 

(define-function QUANTITY.DIMENSION (?q) :-> ?dim 

  "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)." 

  :def (and (physical-quantity ?q)      ; domain constraint 
            (physical-dimension ?dim))  ; range constraint 

  :issues ((:example 
            (= (quantity.dimension (height fred)) length-dimension)))) 

(define-relation COMPATIBLE-QUANTITIES (?x ?y) 

  "Two physical quantities are compatible if their physical-dimensions 
are equal.  Compatibility constrains how quantities can be compared 
and combined with algebraic operators." 

  :iff-def (and (physical-quantity ?x) 
                (physical-quantity ?y) 
                (= (quantity.dimension ?x) (quantity.dimension ?y))) 
  :issues (:example 
           (compatible-quantities (* 6 feet) 
                                  (* 20 meters)))) 

(define-class CONSTANT-QUANTITY (?x) 

  "A constant-quantity is a constant value of some physical-quantity, like 
3 meters or 55 miles per hour. Constant quantities are distinguished from 
function-quantities, which map some quantities to other quantities. 
For example, the velocity of a particle over some range of time would 
be represented by a function-quantity mapping values of time (which are 
constant quantities) to velocity vectors (also constant quantities). 
All real numbers (and numeric tensors of higher order) are constant 
quantities whose dimension is the identity-dimension (i.e., the so-called 
'dimensionless' or nondimensional-constant-quantity). 
  All constant quantites can be expressed as the product of some  
nondimensional quantity and a unit of measure.  This is what it means 
to say a quantity `has a magnitude'.  For example, 2 meters can be expressed  
as (* 3 meter), where meter is defined as a unit of measure for length. 
All units of measure are also constant quantities." 

   ;; constant-quantity is a kind of physical quantity that is not a function 

  :iff-def (and (physical-quantity ?x) 
                (not (function-quantity ?x))) 
  :issues ((:example 
            (constant-quantity (height fred))) 
           ("Why not associate a fixed unit of measure 
             with a quantity?" 
            "Assume that quantities have a property like q.unit. 
             Then define two quantities Q1 = (the-quantity 10 centimeters) 
             and Q2 = (the-quantity 0.1 meters).  Clearly Q1 = Q2. 
             But (q.unit Q1) = centimeters and (q.unit Q2) = meters. 
             This is a contradiction.") 
           ("Why include numbers as quantities?" 
            "This allows one to commit to the engineering math 
             ontologies without having to handle all the units 
             and dimensions.  The theory can include all of normal 
             math as a special case."))) 

(define-class FUNCTION-QUANTITY (?f) 

  "A FUNCTION-QUANTITY is a function that maps from one or more 
constant-quantities to a constant-quantity.  The function must have a 
fixed arity of at least 1.  All elements of the range (ie, values of the 
function) have the same physical-dimension, which is the dimension of 
the function-quantity itself." 

  :iff-def (and (physical-quantity ?f) 

                 ;; an instance of FUNCTION-QUANTITY is a function 
                (function ?f) 
                 ;; the arity is fixed 
                (defined (arity ?f)) 
                 ;; the domains and range of the function are CONSTANT-QUANTITIES 
                (subclass-of (relation-universe ?f) 
                 ;; all the values have the same dimension 
                 ;; the dimension of ?f is the dimension of all of 
                 ;; the values of ?f (ie, instances of its exact-range) 
                (defined (quantity.dimension ?f)) 
                (forall ?val 
                        (=> (instance-of ?val (exact-range ?f)) 
                            (= (quantity.dimension ?f) 
                               (quantity.dimension ?val)))))) 


  "Although it sounds contradictory, a nondimensional-constant-quantity is a 
quantity whose dimension is the identity-dimension.  All numeric tensors,  
including real numbers, are nondimensional quantities." 

  :iff-def (and (constant-quantity ?x) 
                (= (quantity.dimension ?x) identity-dimension)) 

   ;; all real numbers are constant-quantities with the identity-dimension 
   ;; as dimension.   

  :axiom-def (superclass-of nondimensional-constant-quantity real-number)) 

(define-function MAGNITUDE (?q ?unit) :-> ?mag 

  "The magnitude of a constant-quantity is a numeric value for the 
quantity given in terms of some unit-of-measure.  For example, the 
magnitude of the quantity 2 kilometers in the unit-of-measure meter is 
the real number 2000.  The 
unit-of-measure and quantity must be of the same physical-dimension, 
and the resulting value is a nondimensional quantity.  The type of the 
resulting quantity is dependent on the type of the original quantity. 
The magnitude of a scalar-quantity is a real-number, and the magnitude 
of a vector-quantity is a numeric-vector.  In general, then, the 
magnitude function converts a quantity with dimension into a normal 
mathematical object. 
   Units of measure are scalar quantities, and magnitude is defined in 
terms of scalar multiplication.  The magnitude of a quantity in a 
given unit times that unit is equal to the original quantity.  This 
holds for all kinds of tensors, including real-numbers and vectors. 
For scalar quantities, one can think of the magnitude as the ratio of 
a quantity to the unit quantity.  See the definition of the 
multiplication operator * for the various sorts of quantities.  The 
properties of * that hold for all physical-quantities are defined in 
this theory. 
   There is no magnitude for a function-quantity.  Instead, the value 
of a function-quantity on some input is a quantity which may in turn be 
a constant-quantity for which the magnitude function is defined. 
See the definition of value-at." 

  :iff-def (and (constant-quantity ?q) 
		(unit-of-measure ?unit) 
		(nondimensional-constant-quantity ?mag) 
		(compatible-quantities ?q ?unit) 
                (defined (* ?mag ?unit)) 
		(= (* ?mag ?unit) ?q)) 
   ;; magnitudes can be factored out of quantities 
  :axiom-def (forall (?q ?unit ?mag) 
                (=> (and (constant-quantity ?q) 
                         (unit-of-measure ?unit) 
                         (nondimensional-constant-quantity ?mag) 
                         (defined (* ?mag ?q))) 
                    (= (magnitude (* ?mag ?q) ?unit) 
                       (* ?mag (magnitude ?q ?unit))))) 

  :issues ((:example 
	    (=> (= (height fred) (* 2 yards)) 
		(= (magnitude (height fred) feet) 6))))) 

(define-class ZERO-QUANTITY (?x) 

  "A zero quantity is one which, when multiplied times any 
quantity, results in another zero quantity (possibly the same zero). 
The class of zero quantities includes the number 0, and zero 
quantities for every physical dimension and order of tensor." 

  :def (and (physical-quantity ?x) 
	    (forall (?q) 
	       (=> (physical-quantity ?q) 
		   (zero-quantity (* ?q ?x))))) 

  :axiom-def (zero-quantity 0) 

  :issues (("Q: Why not make one zero-thing which follows our 
            "A: We would have to make exceptions for all of our 
                operators on quantities that depend on 
                physical-dimension or tensor-order."))) 

;;;  Operators defined for all physical quantities 

(define-function + (?x ?y):-> ?z 

  "+ 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." 

  :when (and (physical-quantity ?x) 
	     (physical-quantity ?y)) 

  :def (and (physical-quantity ?z) 
            (compatible-quantities ?x ?y) 
            (compatible-quantities ?x ?z))) 

(define-function * (?x ?y):-> ?z 

  "* 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." 

  :when (and (physical-quantity ?x) 
	     (physical-quantity ?y)) 

  :def (and (physical-quantity ?z) 
            (= (quantity.dimension ?z)  
               (* (quantity.dimension ?x) (quantity.dimension ?y))) 

  :axiom-def (and (commutative * physical-quantity) 
                  (associative * physical-quantity) 
                  (distributes * + physical-quantity))) 

(define-function - (?x) :-> ?y 

  "(- ?x) denotes the negative element of element ?x with respect to 
addition operator: i.e., it is the additive inverse.  The unary '-' 
operator for complex numbers (part of KIF specification) is overloaded 
to operate on physical quantities.  All quantity objects have an 
additive inverse and the addition of a parameter and its 
additive-inverse will equal a zero element, such as the real number 0 
or the zero vector of the same dimension if ?x is a vector.  Each 
engineering quantity algebra will define specialization of - for its 

  :when (physical-quantity ?x) 

  :def (and (physical-quantity ?y)  
            (compatible-quantities ?x ?y))) 

(define-function RECIP (?x) :-> ?y 

  "(RECIP ?x) is the reciprocal element of element ?x with respect 
to multiplication operator.  For a number x the reciprocal would be 
1/x.  Not all quantity objects will have a reciprocal element defined. 
The number 0 for instance will not have a reciprocal.  If a parameter 
x has a reciprocal y, then the product of x and y will be an identity 
element of some sort such as '1' for numbers, 3*1/3 = 1.  The 
reciprocal of an element is equivalent to exponentiation of the 
element to the power -1." 

  :when (physical-quantity ?x) 

  :def (and (physical-quantity ?y) 
	    (= (quantity.dimension ?y) (expt (quantity.dimension ?x) -1))) 

  :axiom-def (= (recip ?x) (EXPT ?x -1))) 

(define-function EXPT (?x ?r) :-> ?z 

  "EXPT is exponentiation to real powers for physical-quantities.  The 
'expt' operator for complex numbers (part of KIF specification) is 
overloaded to operate on physical quantities.  This operator is 
further defined for quantity subclasses.  The result is a 
physical-quantity if it is defined." 

  :when (and (physical-quantity ?x) 
	     (real-number ?r)) 
  :def (and (physical-quantity ?z) 
             ;; the dimension of the expt of two quantities is 
             ;; the expt of their dimensions.  See expt below. 
	    (= (quantity.dimension ?z) (expt (quantity.dimension ?x) ?r))) 

  :axiom-def (forall (?x1 ?x2 ?r1 ?r2) 
                  (= (* (EXPT ?x1 ?r1) (EXPT ?x1 ?r2))  
                     (EXPT ?x1 (+ ?r1 ?r2))) 
                  (= (EXPT (* ?x1 ?x2) ?r1)  
                     (* (EXPT ?x1 ?r1) (EXPT ?x2 ?r1))) 
                  (= (EXPT (EXPT ?x1 ?r1) ?r2) 
                     (EXPT ?x1 (* ?r1 ?r2)))))) 

(define-function - (?x ?y) :-> ?z 

  "Subtraction for physical-quantities.  The binary '-' operator for 
complex numbers (part of KIF specification) is overloaded to operate 
on physical quantities.  Defined in terms of addition and unary minus, 

  :when (and (physical-quantity ?x) 
	     (physical-quantity ?y)) 

  := (+ ?x (- ?y))) 

(define-function / (?x ?y):-> ?z 

  "Division for physical-quantities.  The '/' operator for complex 
numbers (part of KIF specification) is overloaded to operate on 
physical quantities.  Defined in terms of multiplication and real 
exponentiation operators." 

  :when (and (physical-quantity ?x) 
	     (physical-quantity ?y)) 
  := (* ?x (EXPT ?y -1))) 

(define-function SUMMATION (?func ?start ?end) :-> ?q 

  "Summation operator for a function that represents an integer 
indexed quantity." 

   ;; this says that summation is total for physical quantities 
  :when (range ?func physical-quantity) 
  :def (and (physical-quantity ?q) 
	    (integer ?start) 
	    (integer ?end))) 

;;; Polymorphic extensions for constant quantities 

  "A relation-extended-to-quantities is a relation that, when it is 
true on a sequence of arguments that are magnitudes (e.g., real numbers or 
tensors), then it is also true on a sequence of constant quantites with those 
magnitudes in some units. 
   For example, the < relation is extended to quantities.  That means 
that for all pairs of quantities q1 and q2, (< q1 q2) if and only  
if (< (magnitude q1 ?u) (magnitude q2 ?u)) for all units on which  
the two magnitudes are defined. 
  There may be relations that are not instances of this class 
that nonetheless hold for quantity arguments.  To be a  
relation-extended-to-quantities means that the relation 
holds when all the arguments are of the same physical dimension." 

  (and (relation ?r) 
       (forall (@args) 
            ;; the relation holds for some constant quantities iff 
           (and (holds ?r @args) 
                (=> (item ?q (listof @args)) 
                    (and (constant-quantity ?q)))) 
            ;; for any unit that is compatible with ALL the arguments 
           (forall (?unit ?q) 
             (=> (and (unit-of-measure ?unit) 
                      (=> (item ?q (listof @args)) 
                          (compatible-quantities ?q ?unit))) 
                  ;; it holds on the magnitudes of those quantities in that unit 
                 (member (map (lambda (?q) (magnitude ?q ?unit)) 
                              (listof @args)) 

(define-relation < (?q1 ?q2) 
  "The < relation is defined for quantities.  It holds on quantities 
when it holds on their magnitudes." 

  :when (and (constant-quantity ?q1) (constant-quantity ?q2)) 
  :axiom-def (relation-extended-to-quantities <)) 

(define-function + (?x ?y):-> ?z 
  "The + function can be applied to all compatible constant quantities. 
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." 

  :when (and (constant-quantity ?x) 
             (constant-quantity ?y)) 
  :axiom-def (relation-extended-to-quantities +) 
   ;; but just to be clear what that means 
  :iff-def (and (constant-quantity ?z) 
                (forall ?unit 
                  (=> (unit-of-measure ?unit) 
                      (= (+ (magnitude ?x ?unit)  
                            (magnitude ?y ?unit)) 
                         (magnitude ?z ?unit)))))) 


(define-class PHYSICAL-DIMENSION (?x) 

  "A physical dimension is a property we associate with physical 
quantities for purposes of classification or differentiation.  Mass, 
length, and force are examples of physical dimensions.  Composite 
physical dimensions can be described by composing primitive dimensions. 
For example, Length/Time ('length over time') is a dimension that can 
be associated with a velocity. 

   The composition operators for dimensions are * [dimension product] 
and expt [exponentiation to a real power], which have algebraic 
properties analogous to their use with real numbers.  The product of 
any two dimensions is a dimension.  There is an indentity element for 
* on dimensions; it is called the identity-dimension.  The product of 
any dimension and the identity-dimension is the original dimension; 
any other product defines a new dimension.  The analogy of division is 
exponentiation to a negative number. 

   There is no intrinsic property of a dimension that makes it primitive. 
A set of primitive dimensions is chosen by convention to define a system 
of units of measure.  However, the relative relationships among 
dimensions can be established independently of systems of units.  For 
example, the dimension corresponding to velocity is length/time, and 
therefore the length dimension is the same as velocity * time.  This is 
true regardless of whether the length or velocity dimensions are viewed 
as the fundamental dimensions in some system, or whether either dimension 
is denoted by a object constant or a term expression in some theory." 

  :def (individual ?x)                                 ;not a set 

  :axiom-def (abelian-group physical-dimension * identity-dimension) 


(define-function * (?d1 ?d2) :-> ?d3 

  "* is a commutative and associative operator for specifying products of 
physical-dimensions.  Together with the identity-dimension, * forms an abelian 
group over physical-dimensions." 

   ;; This :WHEN clause indicates a polymorphic extension of the * operator 
   ;; to the case where it is applied to to dimensions.  The :DEF constraint 
   ;; only holds when the :WHEN condition holds. 

  :when (and (physical-dimension ?d1) 
             (physical-dimension ?d2)) 
  :def (physical-dimension ?d3) 

  :issues ((:example 
            (= force (* mass-dimension length-dimension 
                           (expt time-dimension -2))) 
            (= work (* force length-dimension))))) 

(define-instance IDENTITY-DIMENSION (physical-dimension) 

  "identity-dimension is the identity element for the * operator over 
physical-dimensions.  That means that the product of identity-dimension and 
any other dimension is that other dimension. Identity-dimension is the 
dimension of the so-called dimensionless quantities, including the 
real numbers." 
  :axiom-def (identity-element-for identity-dimension * physical-dimension)) 

(define-function EXPT (?d ?exp) :-> ?dim 

  "Exponentiation of physical-dimensions to a real power." 

  :when (and (physical-dimension ?d) 
	     (real-number ?exp)) 
  :def (physical-dimension ?dim) 

  :axiom-def (forall (?d1 ?d2 ?r1 ?r2) 
                (=> (and (physical-dimension ?d1) 
                         (physical-dimension ?d2) 
                         (real-number ?r1) 
                         (real-number ?r2)) 
                    (and (= (expt ?d1 0) identity-dimension) 
                         (= ?d1 (expt ?d1 1)) 
                         (= (* (expt ?d1 ?r1) (expt ?d1 ?r2))  
                            (expt ?d1 (+ ?r1 ?r2))) 
                         (= (expt (* ?d1 ?d2) ?r1) 
                            (* (expt ?d1 ?r1) (expt ?d2 ?r1))) 
                         (= (expt (expt ?d1 ?r1) ?r2) 
                            (expt ?d1 (* ?r1 ?r2))))))) 


(define-class UNIT-OF-MEASURE (?u) 

  "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." 

  :iff-def (and 
              ;; A unit is a scalar quantity. 
             (constant-quantity ?u) 
              ;; its magnitude is always a positive real, 
              ;; which implies a linear order (not density) 
             (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)))))) 

  :axiom-def (and 
                ;; units can be combined with * to produce units 
               (abelian-group unit-of-measure * identity-unit) 

                ;; any composition of units and reals using * and expt is a unit 
               (=> (and (unit-of-measure ?a) 
                        (real-number ?b)) 
                   (unit-of-measure (* ?a ?b))) 
               (=> (and (unit-of-measure ?a) 
                        (real-number ?b)) 
                   (unit-of-measure (expt ?a ?b))) 

                ;; * is communitive for units and other quantities. 
                ;; This is important for factoring out units 
                ;; when multiplied with tensors or functions. 
               (=> (and (unit-of-measure ?a) 
                        (constant-quantity ?b)) 
                   (= (* ?a ?b) (* ?b ?a))))) 

(define-instance IDENTITY-UNIT (unit-of-measure) 

  "The identity unit can be combined with any other unit to produce 
the same unit.  The identity unit is the real number 1.  Its dimension  
is the identity-dimension." 

  := 1 
  :axiom-def (= (quantity.dimension identity-unit) identity-dimension)) 


(define-class SYSTEM-OF-UNITS (?system) 
  "A system-of-units is a class of units of measure that defines  
a standard system of measurement.  Each instance of the class is a canonical  
unit-of-measure for a dimension.  The mapping from dimensions to units 
in the system is provided by the function called standard-unit; since 
this mapping is functional and total, there is exactly one unit 
in the system of units per dimension. 
   There is no intrinsic property of a dimension that makes it  
fundamental or primitive, and neither is there any such property 
for units of measure.  However, each system of units is defined by 
a basis set of units, from which all other units in the system are 
composed.  The function base-units maps a system-of-units to its basis set. 
The dimensions of the units in the base-set must be orthogonal (see the 
definition of fundamental-dimension-set).  For each composition of  
these fundamental dimensions (e.g., length / time) there is a corresponding  
unique unit in the system-of-units (e.g., meter / second-of-time). 
  The System International (SI) standard used in physics is a system-of-units 
based on seven fundamental dimensions and base units.  Other systems of units 
may have different basis sets of differing cardinality, yet share some of 
the same units as the SI system." 

     ;; a system of units is a CLASS of units 
    (class ?system) 
    (subclass-of ?system unit-of-measure) 
     ;; Every unit in the system is the standard unit for its dimension.  
    (=> (instance-of ?unit ?system) 
        (= (standard-unit ?system (quantity.dimension ?unit)) ?unit)) 

     ;; It defines a set of base units whose dimensions are fundamental 
    (defined (base-units ?system)) 
    (=> (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))))))) 

  :issues ((:example (system-of-units si-unit)) 
           ((("Can any set of units be the base-set for a system of units?" 
              "No, the base-units in a system of units must not be compositions 
               of each other.  For example, if the base units included 
              meter, second-of-time, and (unit* meter second-of-time), then it would 
              NOT be a system of units, because the dimension of 
              (unit* meter second-of-time) is (* length-dimension 
              time-dimension), which is a composition of other 
              ``fundamental'' dimensions."))))) 

(define-function BASE-UNITS (?system-of-units) :-> ?set-of-units 
 "Defines a set of base units for a system of units." 
 :def (and (system-of-units ?system-of-units) 
           (set ?set-of-units) 
           (=> (member ?unit ?set-of-units) 
               (unit-of-measure ?unit)))) 

(define-function STANDARD-UNIT (?system-of-units ?dimension) :-> ?unit 
  "The standard-unit for a given system and dimension is a unit in that  
system whose dimension is the given dimension." 

  :iff-def (and (system-of-units ?system-of-units) 
		(physical-dimension ?dimension) 
		(unit-of-measure ?unit) 
		(instance-of ?unit ?system-of-units) 
		(= (quantity.dimension ?unit) ?dimension))) 

(define-function MAGNITUDE-IN-SYSTEM-OF-UNITS (?q ?system) :-> ?mag 
   "magnitude-in-system-of-units is like magnitude, but it maps a 
quantity and a system of units into a nondimensional numeric value. 
For example, one could ask for the value of 55 miles per hour in the 
SI system.  In SI, the standard-unit for the dimension of miles per hour 
is meters per second-of-time.  So the answer would be about 24 meters per second-of-time." 

   :constraints (and (constant-quantity ?q) 
                     (system-of-units ?system) 
                     (nondimensional-constant-quantity ?mag)) 
   := (magnitude ?q (standard-unit ?system (quantity.dimension ?q)))) 

(define-class ORTHOGONAL-DIMENSION-SET (?set-of-dimensions) 

  "A set of orthogonal dimensions; i.e., dimensions that cannot be 
composed from each other." 

  :iff-def (and (set ?set-of-dimensions) 
                (=> (member ?dim ?set-of-dimensions) 
                      (physical-dimension ?dim) 
                      (not (dimension-composable-from 
                             (difference ?set-of-dimensions (setof ?dim)))))))) 

(define-relation DIMENSION-COMPOSABLE-FROM (?dim ?set-of-dimensions) 
  :iff-def (or (member ?dim ?set-of-dimensions) 
               (exists (?dim1 ?dim2) 
                 (and (dimension-composable-from ?dim1 ?set-of-dimensions) 
                      (dimension-composable-from ?dim2 ?set-of-dimensions) 
                      (= ?dim (* ?dim1 ?dim2)))) 
               (exists (?dim1 ?real) 
                 (and (dimension-composable-from ?dim1 ?set-of-dimensions) 
                      (real-number ?real) 
                      (= ?dim (expt ?dim1 ?real)))))) 

This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber