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 product of two matrices

and also:

If $tau_1$, ..., $tau_n$ denote numbers, then the term {tt (* $tau_1 ldots tau_n$)} denotes the product of those numbers.

Instance-Of: Function

Implication Axioms:

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

Axioms:

(Undefined (Arity *))

(Undefined (Arity *))

(Undefined (Arity *))

(Undefined (Arity *))

Other Related Axioms:

(=> (Defined (* ?E ?Z)) (Zero-Element (* ?E ?Z)))

(=> (Zero-Element ?Z)
    (=> (Defined (* ?E ?Z)) (Zero-Element (* ?E ?Z))))

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

(=> (And (Square-Matrix ?M))
    (= (Determinant ?M)
       (Cond ((= 1 (Size ?M)) (Value ?M 1 1))
             ((< 1 (Size ?M))
              (Summation (Lambda (?J)
                                 (* (Value ?M 1 ?J)
                                    (Cofactor ?M 1 ?J)))
                         1
                         (Size ?M))))))

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

(<=> (Invertible-Matrix ?M)
     (And (Square-Matrix ?M)
          (Exists (?M-1)
                  (And (Square-Matrix ?M-1)
                       (Identity-Matrix (* ?M ?M-1))
                       (Identity-Matrix (* ?M-1 ?M))))))

(=> (= (Matrix-Inverse ?M) ?M-1) (Identity-Matrix (* ?M-1 ?M)))

(=> (= (Matrix-Inverse ?M) ?M-1) (Identity-Matrix (* ?M ?M-1)))