```;;; -*- Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-

;;; Quantity Space
;;; (c) 1993 Greg Olsen and Thomas Gruber

(in-package "ONTOLINGUA-USER")

(define-theory quantity-spaces (physical-quantities)
"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.

This theory defines the class of quantity-space, and the associated
relations POINT-IN, DISTANCE.  It is agnostic about the semantics
of the points -- they needn't be spatial things or of any particular
dimensionality."
:issues ("Copyright (c) 1994 Greg R. Olsen and Thomas R. Gruber"
(:see-also "The EngMath paper on line")))

(in-theory 'quantity-spaces)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Quantity Space
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-class QUANTITY-SPACE (?s)

"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."

:iff-def (and (set ?s)
(forall (?x1 ?x2)
(=> (and (member ?x1 ?s)
(member ?x2 ?s))
(exists (?d)
(and
(= ?d (distance ?x1 ?x2))
(scalar-quantity ?d)))))))

(define-relation POINT-IN (?pt ?sp)
"A point in a quantity-space is simply an element in the set
that is the quantity-space."
:iff-def (and (quantity-space ?sp)
(member ?pt ?sp)))

(define-function DISTANCE (?x1 ?x2) :-> ?d
"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."
:def (and (exists (?sp)
(and (quantity-space ?sp)
(point-in ?x1 ?sp)
(point-in ?x2 ?sp)))
(scalar-quantity ?d))

:axiom-def (and (zero-quantity (distance ?a ?a))
;; commutivity
(= (distance ?b ?c)
(distance ?c ?b))))

```

This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber