Function DISTANCE


Slots on this function:

Documentation:
The DISTANCE function is intended to be polymorphically defined for each quantity space. Its always maps two points in the space to a scalar-quantity. It must be commutative.

and also:

The distance function specialized to points in 3D space.
Instance-Of: Function
Arity: 3

Implication Axioms:

(=> (And (3d-Point ?P1) (3d-Point ?P2))
    (<=> (Distance ?P1 ?P2 ?D)
         (And (Scalar-Quantity ?D)
              (Quantity.Dimension ?D Length-Dimension)
              (= ?D
                 (Sqrt (Dot (Position ?P1 ?P2) (Position ?P1 ?P2)))))))


Axioms:

(Nth-Domain Distance 3 Scalar-Quantity)

(= (Distance ?B ?C) (Distance ?C ?B))

(Zero-Quantity (Distance ?A ?A))


Other Related Axioms:

(=> (And (Member ?X1 3d-Length-Space) (Member ?X2 3d-Length-Space))
    (Quantity.Dimension (Distance ?X1 ?X2) Length-Dimension))

(=> (And (3d-Point ?P1) (3d-Point ?P2))
    (<=> (Distance ?P1 ?P2 ?D)
         (And (Scalar-Quantity ?D)
              (Quantity.Dimension ?D Length-Dimension)
              (= ?D
                 (Sqrt (Dot (Position ?P1 ?P2) (Position ?P1 ?P2)))))))