(define-theory Positions (Localization Topology Quantities))

(in-theory 'Positions)


(DEFINE-RELATION ABOVE (?A ?B)
 "This is a cognitive primitive, derived from 
the up/down schema and not involving contact. 
A possible formalization of the medical meaning must take 
into account the conventional body directions; though, there is no unique 
direction hierarchy guiding the application of this relation to anatomical spaces."
 :DEF (AND (NOT (WEAK-CONTACT ?A ?B)) (POSITION-RELATION ?A ?B)))
(DEFINE-FUNCTION ABSCISSA-VALUE (?A) :-> ?B :DEF
 (AND (EXISTS ?Z (SPATIAL-COORDINATES ?A ?B ?Z)) (POSITION-RELATION ?A ?B))
 :AXIOM-DEF (FUNCTION ABSCISSA-VALUE))
(DEFINE-RELATION ADJACENT-TO (?A ?B)
 "Close to, near or abutting another physical unit with no other 
structure of the same kind intervening. This includes adjoins, abuts, is contiguous to, is 
juxtaposed, and is close to."
 :IFF-DEF (AND (OR (NEAR ?A ?B) (TOUCHES ?A ?B)) (POSITION-RELATION ?A ?B))
 :AXIOM-DEF
 (MAPPING ADJACENT-TO
  "Here adjacency has a wide sense: without contact or with boundary
contact, while 'near' from theory:positions is limited to without contact, and 'externally-connected'
from theory:topology is limited to boundary contact.")
 :AXIOM-CONSTRAINTS
 (AND (RANGE ADJACENT-TO LOCALIZED-ENTITY)
      (DOMAIN ADJACENT-TO LOCALIZED-ENTITY)))
(DEFINE-RELATION ALONG (?A ?B)
 "Along means that an object x shares the region of y 
at least as far the extension of one dimension is concerned."
 :DEF
 (AND (POSITION-RELATION ?A ?B)
      (EXISTS (?C) (AND (GENERICALLY-LOCATED ?A ?C) (IS-REGION-OF ?C ?B)))))
(DEFINE-RELATION APPROACHED-BY (?A ?B) :IFF-DEF
 (= (INVERSE NEAR) APPROACHED-BY))
(DEFINE-RELATION BEHIND (?A ?B)
 "This is a cognitive primitive, derived from the 
front/back schema; a possible formalization of the medical meaning must take into 
account the conventional body directions; though, there is no unique direction 
hierarchy guiding the application of this relation to anatomical spaces."
 :DEF (POSITION-RELATION ?A ?B))
(DEFINE-RELATION BELOW (?A ?B) :IFF-DEF (= (INVERSE ABOVE) BELOW))
(DEFINE-RELATION BETWEEN (?A ?B ?C) :DEF
 (AND (LEFT-OF ?B ?A) (LEFT-OF ?A ?C) (POSITION-TERNARY ?A ?B ?C)) :AXIOM-DEF
 (ARITY BETWEEN 3))
(DEFINE-RELATION CONTAINS (?A ?B) "In USN: 
(:or contains filled-with holds is-occupied-by); for substances mostly. Actually,
the surrounding relation for masses."
 :DEF
 (AND (POSITION-RELATION ?A ?B)
      (EXISTS (?C ?D)
       (AND (INTERIOR ?A ?C) (REGION-OF ?C ?D) (WHOLE-LOCATION-OF ?D ?B)))
      (SUBSTANCE ?B)))
(DEFINE-RELATION CROSSED-OVER-BY (?A ?B) :IFF-DEF
 (= (INVERSE CROSSES-OVER) CROSSED-OVER-BY))
(DEFINE-RELATION CROSSED-THROUGH-BY (?A ?B) :IFF-DEF
 (AND (= (INVERSE CROSSES-THROUGH) CROSSED-THROUGH-BY)
      (LOCALIZED-ENTITY ?A)
      (LOCALIZED-ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE CROSSED-THROUGH-BY LOCALIZED-ENTITY)
      (DOMAIN CROSSED-THROUGH-BY LOCALIZED-ENTITY)))
(DEFINE-RELATION CROSSES-OVER (?A ?B)
 "x crosses-over y when x crosses-through the region of 
y, without overlapping y."
 :DEF
 (AND (EXISTS (?C) (AND (REGION-OF ?B ?C) (CROSSES-THROUGH ?A ?C)))
      (NOT (CONNECTED ?A ?B))
      (POSITION-RELATION ?A ?B)
      (LOCALIZED-ENTITY ?A)
      (LOCALIZED-ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE CROSSES-OVER LOCALIZED-ENTITY)
      (DOMAIN CROSSES-OVER LOCALIZED-ENTITY)))
(DEFINE-RELATION CROSSES-THROUGH (?A ?B)
 "In USN: traverses, which is for 
both crosses-over and crosses-through, for regions or parts only. Here: x crosses-through y 
equals to x overlaps y along at least one whole dimension (length, width or depth), 
say the interiors of x and y overlap.
On the contrary, x crosses-over y equals to x crosses-through the region of y, without 
overlapping y."
 :DEF
 (AND (EXISTS (?C ?D)
       (AND (INTERIOR ?A ?C) (OVERLAPS ?C ?D) (INTERIOR-OF ?D ?B)))
      (POSITION-RELATION ?A ?B)
      (LOCALIZED-ENTITY ?A)
      (LOCALIZED-ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE CROSSES-THROUGH LOCALIZED-ENTITY)
      (DOMAIN CROSSES-THROUGH LOCALIZED-ENTITY)))
(DEFINE-RELATION EVERYWHERE-WITHIN (?A ?B) "" :DEF
 (AND (NOT (EXISTS ?Z
            (AND (EXISTS (?C ?D)
                  (AND (INTERIOR ?A ?D)
                       (REGION-OF ?D ?C)
                       (WHOLLY-LOCATED ?Z ?C)))
                 (DIFFERENT ?Z ?B))))
      (WITHIN ?A ?B)))
(DEFINE-RELATION FACED-BY (?A ?B) :IFF-DEF
 (AND (= (INVERSE ALONG) FACED-BY)
      (LOCALIZED-ENTITY ?A)
      (LOCALIZED-ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE FACED-BY LOCALIZED-ENTITY)
      (DOMAIN FACED-BY LOCALIZED-ENTITY)))
(DEFINE-RELATION FRONT-OF (?A ?B) :IFF-DEF
 (= (INVERSE BEHIND) FRONT-OF))
(DEFINE-RELATION HAS-EVERYWHERE-INSIDE (?A ?B) :IFF-DEF
 (AND (= (INVERSE EVERYWHERE-WITHIN) HAS-EVERYWHERE-INSIDE)
      (LOCALIZED-ENTITY ?A)
      (SUBSTANCE ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE HAS-EVERYWHERE-INSIDE SUBSTANCE)
      (DOMAIN HAS-EVERYWHERE-INSIDE LOCALIZED-ENTITY)))
(DEFINE-RELATION HAS-SOMEWHERE-INSIDE (?A ?B) :IFF-DEF
 (AND (= (INVERSE SOMEWHERE-WITHIN) HAS-SOMEWHERE-INSIDE)
      (LOCALIZED-ENTITY ?A)
      (SUBSTANCE ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE HAS-SOMEWHERE-INSIDE SUBSTANCE)
      (DOMAIN HAS-SOMEWHERE-INSIDE LOCALIZED-ENTITY)))
(DEFINE-RELATION IS-ABSCISSA-VALUE-OF (?A ?B) :IFF-DEF
 (= (INVERSE ABSCISSA-VALUE) IS-ABSCISSA-VALUE-OF))
(DEFINE-RELATION IS-ORDINATE-VALUE-OF (?A ?B) :IFF-DEF
 (= (INVERSE ORDINATE-VALUE) IS-ORDINATE-VALUE-OF))
(DEFINE-RELATION IS-SPATIAL-VALUE-OF (?A ?B) :IFF-DEF
 (= (INVERSE SPATIAL-VALUE) IS-SPATIAL-VALUE-OF))
(DEFINE-RELATION LEFT-OF (?A ?B)
 "This is a cognitive primitive, derived from 
the left/right schema; a possible formalization of the medical meaning must take 
into account the conventional body directions; though, there is no unique direction 
hierarchy guiding the application of this relation to anatomical spaces."
 :DEF (POSITION-RELATION ?A ?B))
(DEFINE-RELATION NEAR (?A ?B)
 "Specialized common sense adjacency without contact; 
based on implicit scale and distance less than the diameter of the smaller object; 
alternatively, based on the smallest distance among the higher granularity objects. 
Eg, in cell C near object P, P is the less distant object of a higher granularity 
than C.
Another possibility is reusing the function topology:neighborhood: (x NEAR y) implies
((REGION-OF (NEIGHBORHOOD x)) loc:OVERLAPS (REGION-OF (NEIGHBORHOOD y))) 
(see 'topologically-near).
Still another: (x NEAR y) implies (x INTERMEDIATE-CONTACT y)."
 :DEF
 (AND (OR (EXISTS (?C ?D ?E)
           (AND (THE-SMALLER ?A ?B ?E)
                (DIAMETER ?E ?D)
                (DISTANCE ?A ?B ?C)
                (< ?C ?D)))
          (NOT (EXISTS ?Z
                (OR (AND (EXISTS (?F)
                          (AND (THE-FINER-GRANULARITY ?A ?Z ?F)
                               (IDENTITY ?F ?A)))
                         (SAME-GRANULARITY ?B ?Z)
                         (EXISTS (?G ?H)
                          (AND (DISTANCE ?B ?A ?H)
                               (DISTANCE ?Z ?A ?G)
                               (< ?G ?H)))
                         (DIFFERENT ?B ?Z))
                    (AND (EXISTS (?I)
                          (AND (THE-FINER-GRANULARITY ?B ?Z ?I)
                               (IDENTITY ?I ?B)))
                         (SAME-GRANULARITY ?A ?Z)
                         (EXISTS (?J ?K)
                          (AND (DISTANCE ?A ?B ?K)
                               (DISTANCE ?Z ?B ?J)
                               (< ?J ?K)))
                         (DIFFERENT ?A ?Z))))))
      (POSITION-RELATION ?A ?B)))
(DEFINE-RELATION ON (?A ?B)
 "This is a cognitive primitive, derived from 
the up/down schema and involving contact.
A possible formalization of the medical meaning must take 
into account the conventional body directions; though, there is no unique direction 
hierarchy guiding the application of this relation to anatomical spaces."
 :DEF (AND (POSITION-RELATION ?A ?B) (WEAK-CONTACT ?A ?B)))
(DEFINE-FUNCTION ORDINATE-VALUE (?A) :-> ?B :DEF
 (AND (EXISTS ?Y (SPATIAL-COORDINATES ?A ?Y ?B)) (POSITION-RELATION ?A ?B))
 :AXIOM-DEF (FUNCTION ORDINATE-VALUE))
(DEFINE-RELATION RIGHT-OF (?A ?B) :IFF-DEF
 (= (INVERSE LEFT-OF) RIGHT-OF))
(DEFINE-RELATION SOMEWHERE-WITHIN (?A ?B) "" :DEF
 (AND (EXISTS ?Z
       (AND (EXISTS (?C ?D)
             (AND (INTERIOR ?A ?D) (REGION-OF ?D ?C) (PART-OF ?Z ?C)))
            (NOT (GENERICALLY-LOCATED ?A ?Z))))
      (WITHIN ?A ?B)))
(DEFINE-RELATION SPATIAL-COORDINATES (?A ?B ?C) :DEF
 (AND (EXISTS (?D) (AND (SPATIAL-VALUE ?A ?D) (= ?B ?D)))
      (EXISTS (?E) (AND (SPATIAL-VALUE ?A ?E) (= ?C ?E)))
      (POSITION-TERNARY ?A ?B ?C))
 :AXIOM-DEF (ARITY SPATIAL-COORDINATES 3))
(DEFINE-FUNCTION SPATIAL-VALUE (?A) :-> ?B :DEF
 (AND (EXISTS ?U
       (AND (SPATIAL-UNIT ?U)
            (EXISTS (?C) (AND (THE-SPATIAL-UNIT ?B ?C) (IDENTITY ?C ?U)))))
      (NUMERIC-VALUE ?A ?B))
 :AXIOM-DEF (FUNCTION SPATIAL-VALUE))
(DEFINE-RELATION SURROUNDED-BY (?A ?B) :IFF-DEF
 (= (INVERSE SURROUNDS) SURROUNDED-BY))
(DEFINE-RELATION SURROUNDS (?A ?B)
 "In USN: (:or limits bounds confines encloses 
circumscribes), but excluding the containment of substances. Here it is
defined by stating that x surrounds y iff the interior of x wholly contains y."
 :DEF
 (AND (NOT (SUBSTANCE ?B))
      (POSITION-RELATION ?A ?B)
      (EXISTS (?C ?D)
       (AND (INTERIOR ?A ?C) (REGION-OF ?C ?D) (WHOLE-LOCATION-OF ?D ?B)))
      (LOCALIZED-ENTITY ?B)))
(DEFINE-RELATION TOPOLOGICALLY-NEAR (?A ?B) :IFF-DEF
 (AND (POSITION-RELATION ?A ?B)
      (EXISTS (?C ?D ?E ?F)
       (AND (NEIGHBORHOOD ?A ?C)
            (REGION-OF ?C ?D)
            (OVERLAPS ?D ?E)
            (IS-REGION-OF ?E ?F)
            (IS-NEIGHBORHOOD-OF ?F ?B)))))
(DEFINE-RELATION TRAVERSED-BY (?A ?B) :IFF-DEF
 (= (INVERSE TRAVERSES) TRAVERSED-BY))
(DEFINE-RELATION TRAVERSES (?A ?B)
 "Crosses or extends across another physical structure or 
area. This includes crosses over and crosses through."
 :DEF
 (AND (POSITION-RELATION ?A ?B) (LOCALIZED-ENTITY ?A) (LOCALIZED-ENTITY ?B))
 :CONSTRAINTS (AND (LOCALIZED-ENTITY ?A) (LOCALIZED-ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE TRAVERSES LOCALIZED-ENTITY)
      (DOMAIN TRAVERSES LOCALIZED-ENTITY)))
(DEFINE-RELATION UNDER (?A ?B) :IFF-DEF
 (AND (= (INVERSE ON) UNDER)
      (LOCALIZED-ENTITY ?A)
      (LOCALIZED-ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE UNDER LOCALIZED-ENTITY)
      (DOMAIN UNDER LOCALIZED-ENTITY)))
(DEFINE-RELATION WITHIN (?A ?B) :IFF-DEF
 (= (INVERSE CONTAINS) WITHIN))