(define-theory Units ())
(in-theory 'Units)


(DEFINE-RELATION SPATIAL-UNIT-OF (?A ?B) :IFF-DEF
 (AND (UNIT-OF ?A ?B) (SPATIAL-UNIT ?A)) :AXIOM-CONSTRAINTS
 (DOMAIN SPATIAL-UNIT-OF SPATIAL-UNIT))
(DEFINE-FUNCTION THE-SPATIAL-UNIT (?A) :-> ?B :IFF-DEF
 (AND (THE-UNIT ?A ?B) (SPATIAL-UNIT ?B)) :AXIOM-DEF
 (FUNCTION THE-SPATIAL-UNIT))
(DEFINE-FUNCTION THE-TIME-UNIT (?A) :-> ?B :IFF-DEF
 (AND (THE-UNIT ?A ?B) (TIME-UNIT ?B)) :AXIOM-DEF (FUNCTION THE-TIME-UNIT))
(DEFINE-FUNCTION THE-UNIT (?A) :-> ?B :DEF
 (AND (EXTRINSIC-STRUCTURING-RELATION ?A ?B) (UNIT ?B)) :AXIOM-DEF
 (FUNCTION THE-UNIT))
(DEFINE-RELATION TIME-UNIT-OF (?A ?B) :IFF-DEF
 (AND (UNIT-OF ?A ?B) (TIME-UNIT ?A)) :AXIOM-CONSTRAINTS
 (DOMAIN TIME-UNIT-OF TIME-UNIT))
(DEFINE-RELATION UNIT-OF (?A ?B) :IFF-DEF
 (= (INVERSE THE-UNIT) UNIT-OF))
(DEFINE-CLASS CURRENCY (?SELF)
:DEF (UNIT ?SELF))
(DEFINE-CLASS DAY (?SELF)
:DEF (TIME-UNIT ?SELF))
(DEFINE-CLASS SPATIAL-UNIT (?SELF)
:DEF (UNIT ?SELF))
(DEFINE-CLASS TIME-UNIT (?SELF)
:DEF (UNIT ?SELF))
(DEFINE-CLASS UNIT (?SELF)
:DEF (SYMBOLIC-STRING ?SELF))