Class QUANTITY-SPACE

• Defined in theory: Quantity-spaces
• Source code: quantity-spaces.lisp

Slots on this class:

Documentation:

A quantity-space is a set that has the property that a distance function is defined for any two elements in the set. In addition, the range of the distance function is a subclass of the class of scalar quantities.

Instance-Of: Class

Subclass-Of: Set

Range-Of: Point-in

Equivalence Axioms:

(<=> (Quantity-Space ?S)
     (And (Set ?S)
          (Forall (?X1 ?X2)
                  (=> (And (Member ?X1 ?S) (Member ?X2 ?S))
                      (Exists (?D)
                              (And (= ?D (Distance ?X1 ?X2))
                                   (Scalar-Quantity ?D)))))))

Axioms:

(Forall (?X1 ?X2)
        (=> (And (Member ?X1 ?S) (Member ?X2 ?S))
            (Exists (?D)
                    (And (= ?D (Distance ?X1 ?X2))
                         (Scalar-Quantity ?D)))))

(Set ?S)

Other Related Axioms:

(<=> (Quantity-Space ?S)
     (And (Set ?S)
          (Forall (?X1 ?X2)
                  (=> (And (Member ?X1 ?S) (Member ?X2 ?S))
                      (Exists (?D)
                              (And (= ?D (Distance ?X1 ?X2))
                                   (Scalar-Quantity ?D)))))))

(=> (Point-In $X $Y) (Quantity-Space $Y))

(<=> (Point-In ?Pt ?Sp) (And (Quantity-Space ?Sp) (Member ?Pt ?Sp)))

(=> (= (Distance ?X1 ?X2) ?D)
    (Exists (?Sp)
            (And (Quantity-Space ?Sp)
                 (Point-In ?X1 ?Sp)
                 (Point-In ?X2 ?Sp))))