Function +

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

Slots on this function:

Documentation:

Function that returns the sum of two matrices

and also:

If $tau_1$, ..., $tau_n$ are numerical constants, then the term {tt (+ $tau_1 ... tau_n$)} denotes the sum $tau$ of the numbers
corresponding to those constants.

Instance-Of: Function

Implication Axioms:

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

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

(=> (= (Cofactor ?M ?I ?J) ?Cof)
    (= ?Cof
       (* (Expt -1 (+ ?I ?J))
          (Determinant (Matrix-Less-Row-And-Column ?M ?I ?J)))))

(=> (= (Matrix-Less-Row ?A ?I) ?B)
    (Forall (?K ?L)
            (=> (Defined (Value ?B ?K ?L))
                (=> (< ?K ?I) (= (Value ?B ?K ?L) (Value ?A ?K ?L)))
                (=> (>= ?K ?I)
                    (= (Value ?B ?K ?L) (Value ?A (+ ?K 1) ?L))))))

(=> (= (Matrix-Less-Column ?A ?I) ?B)
    (Forall (?K ?L)
            (=> (Defined (Value ?B ?K ?L))
                (=> (< ?L ?I) (= (Value ?B ?K ?L) (Value ?A ?K ?L)))
                (=> (>= ?L ?I)
                    (= (Value ?B ?K ?L) (Value ?A ?K (+ ?L 1)))))))