Function -

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

Slots on this function:

Documentation:

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.

Instance-Of: Function

Implication Axioms:

(=> (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))))))))

Axioms:

(Undefined (Arity -))

(Undefined (Arity -))

(Undefined (Arity -))

(Undefined (Arity -))

Other Related Axioms:

(=> (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))))))))

(=> (= (Matrix-Less-Row-And-Column ?A ?I ?J) ?B)
    (= (Column-Dimension ?B) (- (Column-Dimension ?A) 1)))

(=> (= (Matrix-Less-Row-And-Column ?A ?I ?J) ?B)
    (= (Row-Dimension ?B) (- (Row-Dimension ?A) 1)))

(=> (= (Matrix-Less-Row ?A ?I) ?B)
    (= (Row-Dimension ?B) (- (Row-Dimension ?A) 1)))

(=> (= (Matrix-Less-Column ?A ?I) ?B)
    (= (Column-Dimension ?B) (- (Column-Dimension ?A) 1)))