Physical Distance Function

From GM-RKB
Jump to navigation Jump to search

A Physical Distance Function is a Vector Distance Function for the Real World.



References

  • http://www.isi.edu/~hobbs/bgt-space.text
    • In the predicate "distance", we take d to be a non-negative number dependent upon the spatial unit u that is used, rather than reifying distances as distinct entities. We won't say what a spatial unit is, but it can be characterized in the same way temporal units were characterized in Chapter B12. The constraints on the arguments of "distance" are as follows:
      • (2)
  (forall (d x1 x2 u s) 
     (if (distance d x1 x2 u s)
         (and (nonNegativeNumber d)(spatialSystem s)
              (componentOf x1 s)(componentOf x2 s)
              (spatialUnit u s))))

    • We will constrain the predicate "distance" by the usual mathematical properties. The distance between an entity and itself is zero.
      • (3)
  (forall (x u s) (distance 0 x x u s)) 

    • The distance between two entities is symmetric.
      • (4)
  (forall (d x1 x2 u s) 
     (iff (distance d x1 x2 u s)(distance d x2 x1 u s)))

  (forall (d1 d2 d3 d4 x1 x2 x3 u s)
     (if (and (distance d1 x1 x2 u s)(distance d2 x2 x3 u s)
              (distance d3 x1 x3 u s)(sum d4 d1 d2))
         (leq d3 d4)))