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

Scalar-QuantitiesPhysical-QuantitiesFrame-OntologyKif-RelationsKif-SetsKif-ListsKif-NumbersAbstract-AlgebraFrame-Ontology...

**No theories include Vector-Quantities.**

Orthonormal-BasisScalar-ListVector-QuantityNumeric-VectorUnit-Vec3d-Vector-Quantity

**Basis.Dimension****Basis.Vec****Cross****Dot****The-Vector-Quantity****The-Zero-Vector-Of-Type****Vector-Component****Vector-Quantities-Of-Dimensions****Vector.Dimension**

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

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

*Slots Of Instances:*

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

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

Unit length vectors.

**Subclass-Of:**Vector-quantity

**Quantity.Dimension:**Identity-dimension

*Slots Of Instances:*

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

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

*Slots Of Instances:*

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

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

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

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

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

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

**Subclass-Of:**Vector-quantity

**Vector.Dimension:**3

*Slots Of Instances:*

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

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

Formatting and translation code was written by