(define-theory Quantities (Units Physical-Concepts Representation))

(in-theory 'Quantities)


(DEFINE-FUNCTION AGE (?A) :-> ?B :DEF (VALUE ?A ?B) :AXIOM-DEF
 (FUNCTION AGE) :AXIOM-CONSTRAINTS (RANGE AGE VALUE-FILLER))
(DEFINE-FUNCTION AMOUNT (?A) :-> ?B :DEF (NUMERIC-VALUE ?A ?B)
 :AXIOM-DEF (FUNCTION AMOUNT))
(DEFINE-RELATION DEGREE (?A ?B) :IFF-DEF
 (= (INVERSE DEGREE-OF) DEGREE))
(DEFINE-RELATION DEGREE-OF (?A ?B)
 "The relative intensity of a process or the relative intensity 
or amount of a quality or attribute."
 :DEF (QUANTITATIVE-RELATION ?A ?B) :AXIOM-CONSTRAINTS
 (AND (RANGE DEGREE-OF ENTITY)
      (DOMAIN DEGREE-OF ENTITY)))
(DEFINE-FUNCTION DIAMETER (?A) :-> ?B :DEF (NUMERIC-VALUE ?A ?B)
 :AXIOM-DEF (FUNCTION DIAMETER))
(DEFINE-FUNCTION DISTANCE (?A ?B) :-> ?C :DEF
 (AND (EXISTS (?K ?W)
       (AND (STRING ?K) (DISTANCE-MEASURE ?W) (DIMENSIONED-NUMBER ?C ?K ?W)))
      (STRUCTURING-TERNARY ?A ?B ?C)
      (ENTITY ?A)
      (ENTITY ?B)
      (NUMBER ?C))
 :AXIOM-DEF (AND (FUNCTION DISTANCE) (ARITY DISTANCE 3)))
(DEFINE-FUNCTION EXTENT (?A) :-> ?B :DEF (NUMERIC-VALUE ?A ?B)
 :AXIOM-DEF (FUNCTION EXTENT))
(DEFINE-FUNCTION HIGHER-THAN (?A) :-> ?B :DEF
 (AND (EXISTS (?P ?R ?S ?T)
       (AND (RELATION ?P)
            (RELATION ?R)
            (ENTITY ?S)
            (ENTITY ?T)
            (HOLDS-TRUE-3 ?P ?A ?S)
            (HOLDS-TRUE-3 ?R ?B ?T)
            (EXISTS ?Z (AND (SUPERRELATIONS ?P ?Z) (SUPERRELATIONS ?R ?Z)))
            (OR (EXISTS (?C ?D)
                 (AND (NUMERIC-VALUE ?R ?D) (NUMERIC-VALUE ?P ?C) (> ?C ?D)))
                (EXISTS ?Q
                 (AND (SUPERRELATIONS ?Q QUALITATIVE-SCALE)
                      (COMPONENT-OF ?P ?Q)
                      (COMPONENT-OF ?R ?Q))))))
      (QUANTITATIVE-RELATION ?A ?B))
 :AXIOM-DEF (FUNCTION HIGHER-THAN))
(DEFINE-RELATION IS-AGE-OF (?A ?B) :IFF-DEF
 (= (INVERSE AGE) IS-AGE-OF))
(DEFINE-RELATION IS-AMOUNT-OF (?A ?B) :IFF-DEF
 (= (INVERSE AMOUNT) IS-AMOUNT-OF))
(DEFINE-RELATION IS-DIAMETER-OF (?A ?B) :IFF-DEF
 (= (INVERSE DIAMETER) IS-DIAMETER-OF))
(DEFINE-RELATION IS-EXTENT-OF (?A ?B) :IFF-DEF
 (= (INVERSE EXTENT) IS-EXTENT-OF))
(DEFINE-RELATION IS-LENGTH-OF (?A ?B) :IFF-DEF
 (= (INVERSE LENGTH) IS-LENGTH-OF))
(DEFINE-RELATION IS-NUMERIC-VALUE-OF (?A ?B) :IFF-DEF
 (= (INVERSE NUMERIC-VALUE) IS-NUMERIC-VALUE-OF))
(DEFINE-RELATION IS-ORDINAL-VALUE-OF (?A ?B) :IFF-DEF
 (= (INVERSE ORDINAL-VALUE) IS-ORDINAL-VALUE-OF))
(DEFINE-RELATION IS-QUALITATIVE-VALUE-OF (?A ?B) :IFF-DEF
 (= (INVERSE QUALITATIVE-VALUE) IS-QUALITATIVE-VALUE-OF))
(DEFINE-RELATION IS-SERIAL-VALUE-OF (?A ?B) :IFF-DEF
 (= (INVERSE SERIAL-VALUE) IS-SERIAL-VALUE-OF))
(DEFINE-RELATION IS-SIZE-OF (?A ?B) :IFF-DEF
 (= (INVERSE SIZE) IS-SIZE-OF))
(DEFINE-RELATION IS-WIDTH-OF (?A ?B) :IFF-DEF
 (= (INVERSE WIDTH) IS-WIDTH-OF))
(DEFINE-RELATION LARGER (?A ?B) :IFF-DEF
 (= (INVERSE SMALLER) LARGER))
(DEFINE-FUNCTION LENGTH (?A) :-> ?B
 "returns the number of elements in sequence." :DEF (NUMERIC-VALUE ?A ?B)
 :AXIOM-DEF (FUNCTION LENGTH))
(DEFINE-RELATION LOWER-THAN (?A ?B) :IFF-DEF
 (= (INVERSE HIGHER-THAN) LOWER-THAN))
(DEFINE-RELATION MEASURE-VALUE (?A ?B) :IFF-DEF
 (= (INVERSE MEASURE-VALUE-OF) MEASURE-VALUE))
(DEFINE-FUNCTION MEASURE-VALUE-OF (?A) :-> ?B :DEF (VALUE ?A ?B)
 :AXIOM-CONSTRAINTS
 (AND (RANGE MEASURE-VALUE-OF ENTITY)
      (DOMAIN MEASURE-VALUE-OF VALUE-FILLER)))
(DEFINE-RELATION MEASUREMENT (?A ?B) :IFF-DEF
 (AND (EXISTS (?C)
       (AND (MEASURE-VALUE ?A ?C) (EXTRINSICALLY-REPRESENTS ?C ?B)))
      (INVERSE-OF-QUANTITATIVE-RELATION ?A ?B)
      (ENTITY ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE MEASUREMENT ENTITY)
      (DOMAIN MEASUREMENT ENTITY)))
(DEFINE-RELATION MEASUREMENT-OF (?A ?B)
 "The dimension, quantity, or capacity determined by measuring." :IFF-DEF
 (AND (QUANTITATIVE-RELATION ?A ?B)
      (EXISTS (?C)
       (AND (EXTRINSICALLY-REPRESENTED-BY ?A ?C) (MEASURE-VALUE-OF ?C ?B))))
 :AXIOM-DEF
 (MAPPING MEASUREMENT-OF
  "New entry. Probably removable when quantities and dimensions are
systematized. Currently this is defined as the composition of an entity that is 
extrinsically-represented-by (a constant that is the) measure-value-of an entity."))
(DEFINE-FUNCTION MONEY-VALUE (?A ?B) :-> ?C :DEF
 (AND (CURRENCY ?B)
      (EXISTS (?D) (AND (NUMERIC-VALUE ?B ?D) (= ?D ?C)))
      (N-ARY-TUPLE ?A ?B ?C))
 :CONSTRAINTS (AND (ENTITY ?A) (CURRENCY ?B)) :AXIOM-DEF
 (AND (FUNCTION MONEY-VALUE) (ARITY MONEY-VALUE 3))
 :AXIOM-CONSTRAINTS (RANGE MONEY-VALUE NUMBER))
(DEFINE-FUNCTION NUMERIC-VALUE (?A) :-> ?B :DEF
 (AND (VALUE ?A ?B) (NUMBER ?B)) :AXIOM-DEF (FUNCTION NUMERIC-VALUE))
(DEFINE-FUNCTION ORDINAL-VALUE (?A) :-> ?B :DEF
 (AND (NUMERIC-VALUE ?A ?B) (INTEGER ?B)) :AXIOM-DEF (FUNCTION ORDINAL-VALUE))
(DEFINE-RELATION QUALITATIVE-SCALE (?A ?B) :DEF
 (QUANTITATIVE-PROPERTY ?A ?B))
(DEFINE-FUNCTION QUALITATIVE-VALUE (?A) :-> ?B
 "Useful for qualitative scales and in general
symbol sets."
 :DEF (VALUE ?A ?B) :AXIOM-DEF (FUNCTION QUALITATIVE-VALUE))
(DEFINE-RELATION SAME-LEVEL (?A ?B) :DEF
 (AND (EXISTS (?P ?R)
       (AND (PROPERTY ?P)
            (PROPERTY ?R)
            (HOLDS-TRUE-2 ?P ?A)
            (HOLDS-TRUE-2 ?R ?B)
            (IDENTITY ?P ?R)
            (OR (EXISTS (?C ?D)
                 (AND (NUMERIC-VALUE ?R ?D) (NUMERIC-VALUE ?P ?C) (= ?C ?D)))
                (EXISTS ?Q
                 (AND (SUPERRELATIONS ?Q QUALITATIVE-SCALE)
                      (COMPONENT-OF ?P ?Q))))))
      (QUANTITATIVE-RELATION ?A ?B)))
(DEFINE-FUNCTION SERIAL-VALUE (?A) :-> ?B :DEF
 (AND (VALUE ?A ?B) (SERIAL-VALUE-FILLER ?B)) :AXIOM-DEF
 (FUNCTION SERIAL-VALUE))
(DEFINE-FUNCTION SIZE (?A) :-> ?B :DEF (NUMERIC-VALUE ?A ?B)
 :AXIOM-DEF (FUNCTION SIZE))
(DEFINE-RELATION SMALLER (?A ?B) :DEF
 (AND (EXISTS (?C ?D) (AND (SIZE ?A ?D) (SIZE ?B ?C) (> ?C ?D)))
      (QUANTITATIVE-RELATION ?A ?B)))
(DEFINE-FUNCTION THE-HIGHER (?A ?B) :-> ?C :DEF
 (AND (OR (=> (HIGHER-THAN ?A ?B) (IDENTITY ?C ?B))
          (=> (HIGHER-THAN ?B ?A) (IDENTITY ?C ?B)))
      (STRUCTURING-TERNARY ?A ?B ?C))
 :AXIOM-DEF (AND (FUNCTION THE-HIGHER) (ARITY THE-HIGHER 3)))
(DEFINE-FUNCTION THE-SMALLER (?A ?B) :-> ?C :DEF
 (AND (=> (SMALLER ?A ?B) (IDENTITY ?C ?A))
      (=> (SMALLER ?B ?A) (IDENTITY ?C ?B))
      (STRUCTURING-TERNARY ?A ?B ?C))
 :AXIOM-DEF (AND (FUNCTION THE-SMALLER) (ARITY THE-SMALLER 3)))
(DEFINE-FUNCTION WIDTH (?A) :-> ?B :DEF (NUMERIC-VALUE ?A ?B)
 :AXIOM-DEF (FUNCTION WIDTH))
(DEFINE-RELATION _ELONGATE (?A ?B) :IFF-DEF
 (AND (EXISTS (?Y ?Z)
       (AND (EXISTS (?C) (AND (WIDTH ?A ?C) (= ?Z ?C)))
            (EXISTS (?D) (AND (LENGTH ?A ?D) (= ?Y ?D)))
            (> ?Y ?Z)))
      (QUANTITATIVE-PROPERTY ?A ?B)
      (OBJECT ?A)))
(DEFINE-RELATION _FEW (?A ?B)
 "Usable for contextual assessment of numerosity; 
no numeric range can be done, eg compare 'few books on the table' (3?) and 
'few eritrocytes in your blood' (3 millions per part?)."
 :DEF (_PLURALITY ?A ?B))
(DEFINE-RELATION _MANY (?A ?B)
 "Usable for contextual assessment of numerosity; 
no numeric range can be done, eg compare 'many books on the table' (12?) and 
'many eritrocytes in your blood' (8 millions per part?)."
 :DEF (_PLURALITY ?A ?B))
(DEFINE-RELATION _PAIR (?A ?B) :IFF-DEF
 (AND (EXISTS (?C) (AND (NUMERIC-VALUE ?A ?C) (= ?C 2)))
      (QUANTITATIVE-PROPERTY ?A ?B)))
(DEFINE-RELATION _PLURALITY (?A ?B)
 "This property is used to mark plural expressions." :IFF-DEF
 (AND (EXISTS (?C) (AND (NUMERIC-VALUE ?A ?C) (> ?C 1)))
      (QUANTITATIVE-PROPERTY ?A ?B)))
(DEFINE-CLASS AGE-VALUE-FILLER (?SELF)
:DEF (VALUE-FILLER ?SELF))
(DEFINE-CLASS QUANTITATIVE-CONCEPT (?SELF)
:IFF-DEF (MEASURE ?SELF)
 :AXIOM-DEF
 (AND (USN-DOCUMENTATION QUANTITATIVE-CONCEPT
       "A concept which involves the dimensions, quantity or capacity of something using 
some unit of measure, or which involves the quantitative comparison of entities.")
      (MAPPING QUANTITATIVE-CONCEPT
       "Investigate instances: anyway, the theories of units, measures, dimensions etc.
should be used to account for this category.")))
(DEFINE-CLASS QUANTITATIVE-VALUE-FILLER (?SELF)
:DEF (THING ?SELF))
(DEFINE-CLASS SERIAL-VALUE-FILLER (?SELF)
:DEF (VALUE-FILLER ?SELF))
(DEFINE-CLASS VALUE-FILLER (?SELF)
:DEF (CONSTANT ?SELF))