Theory VECTOR-QUANTITIES

This theory is used to represent vectors of n spatial dimensions which are physical quantities with physical dimensions, such as 'the velocity of particle p'. The theory supports arbitrary numbers of basis vector sets and hence vectors are not isomorphic to n-tuples as is the case in some textbook representations of vectors (Note: Multi-basis vector spaces are essential to many theories such as kinematics). Standard vector operations such as vector addition, scalar multiplication, and scalar or dot product are supported. Operators on vector-quantities must take into account the associated units and dimensions.

Source code: vector-quantities.lisp
List of other known theories

Theories included by Vector-Quantities:

    Scalar-Quantities
       Physical-Quantities
          Frame-Ontology
             Kif-Relations
                Kif-Sets
                Kif-Lists
                   Kif-Numbers
          Abstract-Algebra
             Frame-Ontology ...

No theories include Vector-Quantities.

6 classes defined:

    Orthonormal-Basis
    Scalar-List
    Vector-Quantity
       Numeric-Vector
       Unit-Vec
       3d-Vector-Quantity

No relations defined.

No instances defined.

The following constants were used from included theories:

=< defined as a relation in theory Kif-Numbers
Arity defined as a function in theory Frame-Ontology
Class defined as a class in theory Frame-Ontology
Compatible-Quantities defined as a relation in theory Physical-Quantities
Constant-Quantity defined as a class in theory Physical-Quantities
Defined defined as a class in theory Kif-Relations
Documentation defined as a relation in theory Frame-Ontology
Domain defined as a relation in theory Frame-Ontology
First defined as a function in theory Kif-Lists
Function defined as a class in theory Kif-Relations
Function defined as a class in theory Frame-Ontology
Identity-Dimension defined as a object in theory Physical-Quantities
Item defined as a relation in theory Kif-Lists
Length defined as a function in theory Kif-Lists
List defined as a class in theory Kif-Lists
Magnitude defined as a function in theory Physical-Quantities
Nondimensional-Constant-Quantity defined as a class in theory Physical-Quantities
Nth defined as a function in theory Kif-Lists
Nth-Domain defined as a relation in theory Frame-Ontology
Physical-Dimension defined as a class in theory Physical-Quantities
Positive-Integer defined as a class in theory Kif-Numbers
Quantity.Dimension defined as a function in theory Physical-Quantities
Range defined as a relation in theory Frame-Ontology
Scalar-Quantity defined as a class in theory Scalar-Quantities
Subclass-Of defined as a relation in theory Frame-Ontology
Summation defined as a function in theory Physical-Quantities
Summation defined as a function in theory Kif-Relations
The-Zero-Scalar-For-Dimension defined as a function in theory Scalar-Quantities
Unit-Of-Measure defined as a class in theory Physical-Quantities
Value-Cardinality defined as a function in theory Frame-Ontology

All constants that were mentioned were defined.

Class VECTOR-QUANTITY

The class of quantities which are n-dimensional vectors. Each vector has an associated spatial dimension and an associated physical dimension. Each vector-quantity can be decomposed into scalar components for a given orthonormal basis of the proper dimension. The physical-dimension of a scalar component of the vector-quantity is equivalent to the physical-dimension of the vector-quantity.

Subclass-Of: Constant-quantity

Vector.Dimension:: Slot-Cardinality: 1

Axioms:

(<=> (Vector-Quantity ?V) 
     (And (Constant-Quantity ?V) 
          (Value-Cardinality ?V Vector.Dimension 1) 
          (Forall (?B ?I) 
                  (=> (And (Orthonormal-Basis ?B) 
                           (= (Basis.Dimension ?B) 
                              (Vector.Dimension ?V) )
                           (Positive-Integer ?I) 
                           (=< ?I (Vector.Dimension ?V)) )
                      (And (Defined (Vector-Component ?V ?I ?B)) 
                           (= (Quantity.Dimension (Vector-Component ?V
                                                                    ?I
                                                                    ?B))
                              (Quantity.Dimension ?V) ))))
          (Forall (?U) 
                  (=> (And (Unit-Of-Measure ?U) 
                           (= (Quantity.Dimension ?U) 
                              (Quantity.Dimension ?V) ))
                      (Numeric-Vector (Magnitude ?V ?U)) ))))

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Class NUMERIC-VECTOR

A numeric-valued vector. Its components expressed in any basis are numeric or non-dimensional.

Subclass-Of: Nondimensional-constant-quantity, Vector-quantity

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Class UNIT-VEC

Unit length vectors.

Subclass-Of: Vector-quantity

Quantity.Dimension: Identity-dimension

Axioms:

(<=> (Unit-Vec ?V) 
     (And (Vector-Quantity ?V) 
          (= (Quantity.Dimension ?V) Identity-Dimension) 
          (= (Dot ?V ?V) 1) ))

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Function VECTOR.DIMENSION

Function that returns the spatial dimension associated with a vector.

Arity: 2
Domain: Vector-quantity
Range: Positive-integer

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Class ORTHONORMAL-BASIS

A set of n vector-quantities in an n-dimensional vector space which form an ortho-normal basis, the n vector-quantities are linearly independent and the scalar product of any two is the identity-scalar.

Basis.Dimension:: Slot-Cardinality: 1

Axioms:

(=> (Orthonormal-Basis ?B) 
    (And (Forall (?N) 
                 (=> (And (Positive-Integer ?N) 
                          (=< ?N (Basis.Dimension ?B)) )
                     (Defined (Basis.Vec ?B ?N)) ))
         (Forall (?N1 ?N2) 
                 (=> (And (Positive-Integer ?N1) 
                          (Positive-Integer ?N2) 
                          (=< ?N1 (Basis.Dimension ?B)) 
                          (=< ?N2 (Basis.Dimension ?B)) )
                     (=> (= ?N1 ?N2) 
                         (= (Dot (Basis.Vec ?B ?N1) 
                                 (Basis.Vec ?B ?N2) )
                            1 ))
                     (=> (/= ?N1 ?N2) 
                         (= (Dot (Basis.Vec ?B ?N1) 
                                 (Basis.Vec ?B ?N2) )
                            0 ))))))

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Function BASIS.VEC

Function to select the individual unit vectors of a basis.

Arity: 3

Axioms:

(Nth-Domain Basis.Vec 3 Unit-Vec) 

(Nth-Domain Basis.Vec 2 Positive-Integer) 

(Nth-Domain Basis.Vec 1 Orthonormal-Basis) 

(=> (Basis.Vec ?Basis ?N ?Uv) (=< ?N (Basis.Dimension ?Basis)))

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Function BASIS.DIMENSION

Function that returns the spatial dimension associated with a basis set of vectors.

Arity: 2
Domain: Orthonormal-basis
Range: Positive-integer

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Function VECTOR-COMPONENT

Function to generate the ith scalar component for a vector-quantity in a particular basis.

Arity: 4

Axioms:

(Nth-Domain Vector-Component 4 Scalar-Quantity) 

(Nth-Domain Vector-Component 3 Orthonormal-Basis) 

(Nth-Domain Vector-Component 2 Positive-Integer) 

(Nth-Domain Vector-Component 1 Vector-Quantity) 

(<=> (Vector-Component ?V ?I ?B ?S) 
     (And (Vector-Quantity ?V) 
          (Positive-Integer ?I) 
          (Orthonormal-Basis ?B) 
          (Scalar-Quantity ?S) 
          (= (Quantity.Dimension ?S) (Quantity.Dimension ?V)) 
          (= (Vector.Dimension ?V) (Basis.Dimension ?B)) 
          (=< ?I (Vector.Dimension ?V)) 
          (= ?S (Dot ?V (Basis.Vec ?B ?I))) ))

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Function THE-VECTOR-QUANTITY

Constructor function for a vector-quantity with scalar components ?sl in ortonormal basis ?b.

Arity: 3

Axioms:

(Nth-Domain The-Vector-Quantity 3 Vector-Quantity) 

(Nth-Domain The-Vector-Quantity 2 Orthonormal-Basis) 

(Nth-Domain The-Vector-Quantity 1 Scalar-List) 

(<=> (The-Vector-Quantity ?Sl ?B ?V) 
     (And (Scalar-List ?Sl) 
          (Orthonormal-Basis ?B) 
          (Vector-Quantity ?V) 
          (= (Quantity.Dimension ?V) 
             (Quantity.Dimension (First ?Sl)) )
          (= (Length ?Sl) (Basis.Dimension ?B)) 
          (= (Vector.Dimension ?V) (Length ?Sl)) 
          (= (Nth ?Sl ?I) (Vector-Component ?V ?I ?B)) 
          (= ?V
             (Summation (Lambda (?J) 
                                (* (Nth ?Sl ?J) (Basis.Vec ?B ?J)) )
                        1 
                        (Vector.Dimension ?V) ))))

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Class SCALAR-LIST

Class of ordered sequences of the scalars of a common physical dimension.

Subclass-Of: List

Axioms:

(<=> (Scalar-List ?Sl) 
     (And (List ?Sl) 
          (Forall (?S) (=> (Item ?S ?Sl) (Scalar-Quantity ?S))) 
          (Forall (?S1 ?S2) 
                  (=> (And (Item ?S1 ?Sl) (Item ?S2 ?Sl)) 
                      (Compatible-Quantities ?S1 ?S2) ))))

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Function THE-ZERO-VECTOR-OF-TYPE

The ?spatdim dimensional zero vector of physical dimension ?physdim.

Arity: 3

Axioms:

(Nth-Domain The-Zero-Vector-Of-Type 2 Physical-Dimension) 

(Nth-Domain The-Zero-Vector-Of-Type 1 Positive-Integer) 

(Nth-Domain The-Zero-Vector-Of-Type 3 Vector-Quantity) 

(=> (The-Zero-Vector-Of-Type ?Spatdim ?Physdim ?V0) 
    (Forall (?V) 
            (=> (Vector-Quantity ?V) 
                (= (Dot ?V ?V0) 
                   (The-Zero-Scalar-For-Dimension ?Physdim) ))))

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Function VECTOR-QUANTITIES-OF-DIMENSIONS

Arity: 3

Axioms:

(= (Vector-Quantities-Of-Dimensions ?Physim ?Spatdim) 
   (If (And (Physical-Dimension ?Physim) (Positive-Integer ?Spatdim)) 
       (Kappa (?Vq) 
              (And (Vector-Quantity ?Vq) 
                   (= (Vector.Dimension ?Vq) ?Spatdim) 
                   (= (Quantity.Dimension ?Vq) ?Physim) ))))

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Function DOT

Vector-Quantity dot or scalar product. Generalizes to inner-product. This product is only defined for vectors of a common spatial dimension. The physical dimension of the product is the product of the dimensions of the argument vectors. The product is the sum of the products of the corresponding scalar components of the argument vectors for a common basis.

Arity: 3

Axioms:

(Nth-Domain Dot 3 Scalar-Quantity) 

(Nth-Domain Dot 2 Vector-Quantity) 

(Nth-Domain Dot 1 Vector-Quantity) 

(=> (Dot ?V1 ?V2 ?S) 
    (And (= (Vector.Dimension ?V1) (Vector.Dimension ?V2)) 
         (= (Quantity.Dimension ?S) 
            (* (Quantity.Dimension ?V1) (Quantity.Dimension ?V2)) )
         (Forall (?B) 
                 (=> (= (Basis.Dimension ?B) (Vector.Dimension ?V1)) 
                     (= ?S
                        (Summation (Lambda (?J) 
                                           (* (Vector-Component ?V1
                                                                ?J
                                                                ?B)
                                              (Vector-Component ?V2
                                                                ?J
                                                                ?B)))
                                   1 
                                   (Vector.Dimension ?V1) ))))))

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Class 3D-VECTOR-QUANTITY

Vectors of 3-dimensions. (These vectors have important properities and are of particular interest to engineering analysis).

Subclass-Of: Vector-quantity

Vector.Dimension: 3

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

Function CROSS

Vector or cross product of two three dimensional vectors. If we know the components of two vectors with respect to a common basis, we can determine the components of the cross product in that basis.

Arity: 3

Axioms:

(Nth-Domain Cross 3 3d-Vector-Quantity) 

(Nth-Domain Cross 2 3d-Vector-Quantity) 

(Nth-Domain Cross 1 3d-Vector-Quantity) 

(=> (Cross ?V1 ?V2 ?V) 
    (And (= (Quantity.Dimension ?V) 
            (* (Quantity.Dimension ?V1) (Quantity.Dimension ?V2)) )
         (= (Dot ?V1 ?V) 
            (The-Zero-Scalar-For-Dimension (* (Quantity.Dimension ?V1)
                                              (Quantity.Dimension ?V) )))
         (= (Dot ?V2 ?V) 
            (The-Zero-Scalar-For-Dimension (* (Quantity.Dimension ?V2)
                                              (Quantity.Dimension ?V) )))
         (= (Vector-Component ?V 1 ?B) 
            (- (* (Vector-Component ?V1 2 ?B) 
                  (Vector-Component ?V2 3 ?B) )
               (* (Vector-Component ?V2 2 ?B) 
                  (Vector-Component ?V1 3 ?B) )))
         (= (Vector-Component ?V 2 ?B) 
            (- (* (Vector-Component ?V2 1 ?B) 
                  (Vector-Component ?V1 3 ?B) )
               (* (Vector-Component ?V1 1 ?B) 
                  (Vector-Component ?V2 3 ?B) )))
         (= (Vector-Component ?V 3 ?B) 
            (- (* (Vector-Component ?V1 1 ?B) 
                  (Vector-Component ?V2 2 ?B) )
               (* (Vector-Component ?V2 1 ?B) 
                  (Vector-Component ?V1 2 ?B) )))))

Defined in theory: Vector-quantities
Source code: vector-quantities.lisp

This document was generated using Ontolingua.
Formatting and translation code was written by

François Gerbaux and Tom Gruber