Function -

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

Slots on this function:

Documentation:

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.

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