(define-theory Localization (Mereology))
(in-theory 'Localization)



(DEFINE-RELATION HAS-ADDRESS (?A ?B)
 "Another metonymic use of location: some (intentional) 
entity chooses one of its possible addresses for social and legal purposes. Currently
not axiomatized (issues: temporariness of localization, electivity, social relevance).
Example issues: physical persons are wholly located at an address, but that address is 
temporary at the interesting temporal granularity, while organizations are usually 
partly located at a main or default address, but that address is permanent at the 
interesting granularity. On the other hand, consider that from some social and
legal aspects actual presence is not required (mailing, messages, estates, ...)."
 :DEF (LOCATIVE-RELATION ?A ?B) :AXIOM-CONSTRAINTS
 (AND (RANGE HAS-ADDRESS ADDRESS)
      (DOMAIN HAS-ADDRESS SOCIAL-OBJECT)))
(DEFINE-RELATION ADDRESS-OF (?A ?B) :IFF-DEF
 (= (INVERSE HAS-ADDRESS) ADDRESS-OF))
(DEFINE-RELATION EXACT-LOCATION-OF (?A ?B) :IFF-DEF
 (AND (EXISTS (?C) (AND (LOCATION-OF ?A ?C) (PART-OF ?C ?B)))
      (LOCATION-OF ?A ?B)
      (WHOLE-LOCATION-OF ?A ?B)
      (REGION ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE EXACT-LOCATION-OF ENTITY)
      (DOMAIN EXACT-LOCATION-OF REGION)))
(DEFINE-RELATION EXACTLY-LOCATED (?A ?B)
 "The actual, minimal localization, where the range is 
necessarily a region. A more specialized notion of 'location'."
 :IFF-DEF (AND (WHOLLY-LOCATED ?A ?B) (PARTLY-LOCATED ?A ?B) (REGION ?B)))
(DEFINE-RELATION GENERIC-LOCATION-OF (?A ?B) :IFF-DEF
 (AND (EXISTS (?C ?D)
       (AND (PART ?A ?C) (LOCATION-OF ?C ?D) (PART-OF ?D ?B)))
      (ENTITY ?A)
      (LOCATION-OF ?A ?B)
      (REGION ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE GENERIC-LOCATION-OF ENTITY)
      (DOMAIN GENERIC-LOCATION-OF REGION)))
(DEFINE-RELATION GENERICALLY-LOCATED (?A ?B)
 "The general case: part of something is located at 
part of something."
 :IFF-DEF
 (AND (LOCATED ?A ?B)
      (EXISTS (?C ?D) (AND (PART ?A ?C) (LOCATED ?C ?D) (PART-OF ?D ?B)))
      (REGION ?B)))
(DEFINE-RELATION IS-REGION-OF (?A ?B) :IFF-DEF
 (AND (= (INVERSE REGION-OF) IS-REGION-OF)
      (REGION ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE IS-REGION-OF ENTITY)
      (DOMAIN IS-REGION-OF REGION)))
(DEFINE-RELATION UNIQUE-LOCATION (?A ?B) :IFF-DEF
 (IS-REGION-OF ?A ?B))
(DEFINE-RELATION UNIQUE-LOCATION-OF (?A ?B) :IFF-DEF
 (IS-REGION-OF ?A ?B))
(DEFINE-RELATION LOCATED (?A ?B)
 "The actual, minimal localization, where the range is 
necessarily a region."
 :DEF (AND (LOCATIVE-RELATION ?A ?B) (REGION ?B)))
(DEFINE-RELATION LOCATION-OF (?A ?B) :IFF-DEF
 (= (INVERSE LOCATED) LOCATION-OF))
(DEFINE-RELATION OVERLAPS (?A ?B)
 "This overlapping relation is for regions only, 
thus it is not counterintuitive (in mereology, 'common-part' is better, because
common sense talks of overlap also between externally connected objects)."
 :DEF (AND (COMMON-PART ?A ?B) (REGION ?A) (REGION ?B)))
(DEFINE-RELATION PARTIAL-LOCATION-OF (?A ?B) :IFF-DEF
 (AND (EXISTS (?C) (AND (LOCATION-OF ?A ?C) (PART-OF ?C ?B)))
      (LOCATION-OF ?A ?B)
      (REGION ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE PARTIAL-LOCATION-OF ENTITY)
      (DOMAIN PARTIAL-LOCATION-OF REGION)))
(DEFINE-RELATION PARTLY-LOCATED (?A ?B)
 "The partial localization: Istanbul is partly in Asia." :IFF-DEF
 (AND (EXISTS (?C) (AND (PART ?A ?C) (LOCATED ?C ?B)))
      (LOCATED ?A ?B)
      (ENTITY ?A)
      (REGION ?B))
 :CONSTRAINTS (AND (ENTITY ?A) (REGION ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE PARTLY-LOCATED REGION)
      (DOMAIN PARTLY-LOCATED ENTITY)))
(DEFINE-RELATION REFERENCE-LOCATION (?A ?B)
 "The main metonymic use of location: anything can
be (wholly, partly, or generically, but not exactly) located at some entity's 
region."
 :IFF-DEF
 (AND (LOCATIVE-RELATION ?A ?B)
      (EXISTS (?C) (AND (LOCATED ?A ?C) (IS-REGION-OF ?C ?B)))))
(DEFINE-RELATION REFERENCE-LOCATION-OF (?A ?B) :IFF-DEF
 (AND (EXISTS (?C) (AND (REGION-OF ?A ?C) (LOCATION-OF ?C ?B)))
      (INVERSE-OF-LOCATIVE-RELATION ?A ?B)
      (ENTITY ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE REFERENCE-LOCATION-OF ENTITY)
      (DOMAIN REFERENCE-LOCATION-OF ENTITY)))
(DEFINE-FUNCTION REGION-OF (?A) :-> ?B
 "The region where x is uniquely located: the 
position of something. This results as a constrained functional counterpart
of 'exactly-located."
 :DEF
 (AND (NOT (EXISTS ?Z (AND (EXACTLY-LOCATED ?A ?Z) (IDENTITY ?B ?Z))))
      (EXACTLY-LOCATED ?A ?B))
 :AXIOM-DEF (FUNCTION REGION-OF))
(DEFINE-FUNCTION UNIQUELY-LOCATED (?A) :-> ?B
 "The region where x is uniquely located: the 
position of something. This results as a constrained functional counterpart
of 'exactly-located."
 :IFF-DEF (REGION-OF ?A ?B))
(DEFINE-RELATION SAME (?A ?B)
 "Identity of regions is reciprocal parthood." :IFF-DEF
 (AND (PART-OF ?A ?B) (PART ?A ?B) (REGION ?A) (REGION ?B)))
(DEFINE-RELATION SCATTERED-LOCATION (?A ?B)
 "A metonymic use of location ranging over the region
of the parts of scattered entities. For instance, when one says that a population is 
the location of a pathology or an anatomical abnormality."
 :DEF
 (AND (LOCATIVE-RELATION ?A ?B)
      (EXISTS (?C) (AND (REFERENCE-LOCATION ?A ?C) (PART-OF ?C ?B)))))
(DEFINE-RELATION SCATTERED-LOCATION-OF (?A ?B) :IFF-DEF
 (AND (= (INVERSE SCATTERED-LOCATION) SCATTERED-LOCATION-OF)
      (ENTITY ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE SCATTERED-LOCATION-OF ENTITY)
      (DOMAIN SCATTERED-LOCATION-OF ENTITY)))
(DEFINE-RELATION WHOLE-LOCATION-OF (?A ?B) :IFF-DEF
 (AND (EXISTS (?C) (AND (PART ?A ?C) (LOCATION-OF ?C ?B)))
      (ENTITY ?A)
      (LOCATION-OF ?A ?B)
      (REGION ?A)
      (ENTITY ?B))
 :CONSTRAINTS (AND (REGION ?A) (ENTITY ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE WHOLE-LOCATION-OF ENTITY)
      (DOMAIN WHOLE-LOCATION-OF REGION)))
(DEFINE-RELATION WHOLLY-LOCATED (?A ?B)
 "The non-minimal localization: Nick is in Rome." :IFF-DEF
 (AND (EXISTS (?C) (AND (LOCATED ?A ?C) (PART-OF ?C ?B)))
      (ENTITY ?B)
      (LOCATED ?A ?B)
      (ENTITY ?A)
      (REGION ?B))
 :CONSTRAINTS (AND (ENTITY ?A) (REGION ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE WHOLLY-LOCATED REGION)
      (DOMAIN WHOLLY-LOCATED ENTITY)))
(DEFINE-CLASS ADDRESS (?SELF)
 "A topographic location, generally having definite boundaries
and with a finer detail than a geographic area. This concept is enough to represent the state
of 'being at an address'. The relation for 'having an address' is a more complex issue, since 
having an address does not imply being at that address all the time (or a default amount of 
time). Instead having an address implies a social and legal responsibility for being retrievable,
receiving mail, being contacted, having own estates localized, etc."
 :DEF
 (AND (REGION ?SELF)
      (EXISTS (?A) (AND (CONVENTIONAL-WITHIN ?SELF ?A) (TOPOGRAPHY ?A)))))
(DEFINE-CLASS GEOGRAPHIC-AREA (?SELF)
 "A geographic location, generally having definite boundaries." :DEF
 (AND (REGION ?SELF)
      (EXISTS (?A) (AND (CONVENTIONAL-WITHIN ?SELF ?A) (GEOGRAPHY ?A)))))
(DEFINE-CLASS REGION (?SELF)
 "A region is the only entity which can be located at 
itself."
 :DEF (LOCALIZED-ENTITY ?SELF) :CONSTRAINTS
 (AND (VALUE-TYPE ?SELF LOCATED REGION)
      (VALUE-TYPE ?SELF PART REGION)
      (EXISTS (?A) (AND (PROPER-PART ?SELF ?A) (REGION ?A)))
      (EXISTS (?B) (AND (PROPER-PART-OF ?SELF ?B) (REGION ?B))))
 :AXIOM-DEF (MAPPING REGION "USN 'spatial-concept' can be mapped here."))