Function -

• Defined in theory: Tensor-quantities
• Source code: tensor-quantities.lisp
• Also defined in: Kif-numbers, Dme-kb, Basic-matrix-algebra, Physical-quantities

Slots on this function:

Documentation:

- is the binary subtraction operator for physical-quantities. This is a polymorphic extension of the same function over real numbers as defined in the kif-numbers ontology.

All quantity objects have an additive inverse and the addition of a parameter and its additive-inverse will equal a zero element, such as the real number 0 or the zero vector of the same dimension if ?x is a vector. Each engineering quantity algebra will define specialization of + for its domain wirth a zero element.

and also:

If $tau$ and $tau_1$, ..., $tau_n$ denote numbers, then the term {tt (- $tau$ $tau_1 ... tau_n$)} denotes the difference between the
number denoted by $tau$ and the numbers denoted by $tau_1$ through $tau_n$. An exception occurs when $n=0$, in which case the term denotes the negation of the number denoted by $tau$.

and also:

The - function is also defined for matrices, where it means the difference between two matrices (in the binary case) or additive inverse in the unary case.

and also:

The unary minus function is also defined for vector quantities.

Instance-Of: Function

Implication Axioms:

(=> (And (Physical-Quantity ?X) (Physical-Quantity ?Y))
    (<=> (- ?X ?Y ?Z) (= ?X (+ ?Y ?Z))))

(=> (Matrix ?A)
    (<=> (- ?A ?C)
         (And (Matrix ?C)
              (Forall (?I ?J)
                      (=> (Defined (Value ?C ?I ?J))
                          (= (Value ?C ?I ?J) (- (Value ?A ?I ?J))))))))

(=> (And (Matrix ?A)
         (Matrix ?B)
         (= (Row-Dimension ?A) (Row-Dimension ?B))
         (= (Column-Dimension ?A) (Column-Dimension ?B)))
    (<=> (- ?A ?B ?C)
         (And (Matrix ?C)
              (= (Row-Dimension ?A) (Row-Dimension ?C))
              (= (Column-Dimension ?A) (Column-Dimension ?C))
              (Forall (?I ?J)
                      (=> (Defined (Value ?C ?I ?J))
                          (= (Value ?C ?I ?J)
                             (- (Value ?A ?I ?J) (Value ?B ?I ?J))))))))

(=> (And (Vector-Quantity ?X) (- ?X ?Y))
    (And (Vector-Quantity ?Y)
         (= (+ ?X ?Y)
            (The-Zero-Vector-Of-Type (Quantity.Dimension ?X)
                                     (Spatial.Dimension ?X)))))

Axioms:

(Undefined (Arity -))

(Undefined (Arity -))

(Undefined (Arity -))

(Undefined (Arity -))

(Undefined (Arity -))

(Undefined (Arity -))

(Undefined (Arity -))

(Undefined (Arity -))

Other Related Axioms:

(=> (And (Vector-Quantity ?X) (- ?X ?Y))
    (And (Vector-Quantity ?Y)
         (= (+ ?X ?Y)
            (The-Zero-Vector-Of-Type (Quantity.Dimension ?X)
                                     (Spatial.Dimension ?X)))))