*;;; -*- 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