```;;; -*- Mode:Lisp; Syntax:Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-

;;; Matrix-Algebra Ontology
;;; (c) 1993,1994  Gregory R. Olsen, Yves Peligry, and Thomas R. Gruber

(in-package "ONTOLINGUA-USER")

(define-theory basic-matrix-algebra (frame-ontology)
"This theory attempts to capture basic concepts in linear algebra, with
emphasis on matrix operations.  Definitions are derived from, Strang, G.,
Linear Algebra and its Applications, 3rd Edition, Harcourt Brace Jovanovich,
1988."
:issues ("(c) 1993, 1994 Gregory R. Olsen, Yves Peligry, and Thomas R. Gruber"
(:see-also "The EngMath paper on line")))

(in-theory 'basic-matrix-algebra)

;; This def probably belongs somewhere else like kif-misc
(define-class ZERO-ELEMENT (?z)
"Class that contains all elements we associate with zero, e.g. the number
zero, matrices full of zero elements, or quantities of various dimension with
zero magnitude.  All these elements behave similarly with respect to the
multiplication operator '*', but differentiation between them allows regularity
in algebraic rules (e.g. dimensions of operands and product in matrix
multiplication).
The product of a zero-element and anything (when the product is defined)
is another zero-element (not necessarily the same).  For example, if A
is a 1xN matrix and B is a NxN zero matrix, then the product A*B is a 1XN
zero matrix."
:def (=> (defined (* ?e ?z))
(zero-element (* ?e ?z)))
:axiom-def (zero-element 0))

(define-class MATRIX (?M)
"A matrix is a binary function mapping pairs of integers (its indices) to
some value.  It is total for integers from 1 to some constant bound, for its
row and column indices.  Each matrix has a row and a column dimension"

:iff-def (and (function ?M)
(= (arity ?M) 3)
(positive-integer (row-dimension ?M))
(positive-integer (column-dimension ?M))

(=> (and (positive-integer ?i)
(positive-integer ?j)
(=< ?i (row-dimension ?M))
(=< ?j (column-dimension ?M)))
(defined (value ?M ?i ?j)))))

(define-function ROW-DIMENSION (?m) :-> ?i
"The number of rows in a matrix."
:def (and (matrix ?m)
(positive-integer ?i)))

(define-function COLUMN-DIMENSION (?m) :-> ?i
"The number of columns in a matrix."
:def (and (matrix ?m)
(positive-integer ?i)))

(define-class ROW-MATRIX (?M)
"Class of the matrices with only one row"
:iff-def (and (matrix ?M)
(= (row-dimension ?M) 1)))

(define-class COLUMN-MATRIX (?M)
"Class of the matrices with only one column"
:iff-def (and (matrix ?M)
(= (column-dimension ?M) 1)))

;;;----------------------------------------------------------------------
;;; Operations on matrices
;;;----------------------------------------------------------------------

(define-function MATRIX-OF-ROWS (@elements) :-> ?M
"Constructor for matrices.  The arguments are a list of rows in the matrix."
:iff-def (and (matrix ?M)
(= (row-dimension ?M) (length (listof @elements)))
(= (row ?i ?M) (nth (listof @elements) ?i))
(=> (and (item ?e1 (listof @elements))
(item ?e2 (listof @elements)))
(= (column-dimension ?e1)
(column-dimension ?e2)))))

(define-function MATRIX-OF-COLUMNS (@elements) :-> ?M
"Constructor for matrices.  The arguments are a list of columns in
the matrix."
:iff-def (and (matrix ?M)
(= (column-dimension ?M) (length (listof @elements)))
(= (column ?i ?M) (nth (listof @elements) ?i))
(=> (and (item ?e1 (listof @elements))
(item ?e2 (listof @elements)))
(= (row-dimension ?e1)
(row-dimension ?e2)))))

(define-function TRANSPOSE (?A) :-> ?B
"Function that returns the matrix with lines and columns interchanged
the matrix (1 3)  would be transformed into the matrix (1 2)
(2 7)                                       (3 7)"
:iff-def (and (matrix ?A)
(matrix ?B)
(= (column-dimension ?A) (row-dimension ?B))
(= (row-dimension ?A) (column-dimension ?B))
(forall (?i ?j)
(= (value ?A ?i ?j) (value ?B ?j ?i)))))

(define-function ROW (?M ?i) :-> ?L
"Function that returns the i-th row of a given matrix"
:iff-def (and (matrix ?M)
(positive-integer ?i)
(=< ?i (row-dimension ?M))
(row-matrix ?L)
(= (column-dimension ?M)
(column-dimension ?L))
(forall ?j (= (value ?M ?i ?j) (value ?L 1 ?j)))))

(define-function COLUMN (?M ?i) :-> ?L
"Function that returns the i-th column of a given matrix"
:iff-def (and (matrix ?M)
(positive-integer ?i)
(=< ?i (column-dimension ?M))
(column-matrix ?L)
(= (row-dimension ?M)
(row-dimension ?L))
(forall ?j (= (value ?M ?j ?i) (value ?L ?j 1)))))

(define-class SQUARE-MATRIX (?M)
"Class of the matrices whose number of columns is equal to the number
of rows"
:iff-def (and (matrix ?M)
(= (column-dimension ?M)
(row-dimension ?M))))

(define-function SIZE (?M) :-> ?n
"Size is the number of row or column of a square matrix"
:iff-def (and (square-matrix ?M)
(= ?n (row-dimension ?M))))

(define-class IDENTITY-MATRIX (?IM)
"Identity matrix is a class because it is not unique (one per size)
it is a matrix with only 1 on the diagonal and 0 everywhere else"
:iff-def (and	(square-matrix ?IM)
(forall (?i ?J)
(=> (defined (value ?IM ?i ?j))
(and
(=> (= ?i ?j) (= (value ?IM ?i ?j) 1))
(=> (/= ?i ?j)
(zero-element (value ?IM ?i ?j))))))))

(define-class DIAGONAL-MATRIX (?M)
"A diagonal-matrix is a matrix with 0 apart from the diagonal"
:iff-def (and (matrix ?M)
(square-matrix ?M)
(forall (?i ?j)
(=> (and (defined (value ?M ?i ?j))
(/= ?i ?j))
(zero-element (value ?M ?i ?j))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;  Matrix Operators
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-function * (?A ?B) :-> ?C
"Function that returns the product of two matrices"
:when (and (matrix ?A)
(matrix ?B)
(= (column-dimension ?A) (row-dimension ?B)))

:iff-def (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)))))))

(define-function + (?A ?B) :-> ?C
"Function that returns the sum of two matrices"
:when (and (matrix ?A)
(matrix ?B)
(= (row-dimension ?A) (row-dimension ?B))
(= (column-dimension ?A) (column-dimension ?B)))

:iff-def (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)))))))

(define-function - (?A ?B) :-> ?C
"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."
:when (and (matrix ?A)
(matrix ?B)
(= (row-dimension ?A) (row-dimension ?B))
(= (column-dimension ?A) (column-dimension ?B)))

:iff-def (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))))))
:axiom-def
;; :when (matrix ?A)
(=> (matrix ?a)
(<=> (- ?a ?c)
(and (matrix ?C)
(forall (?i ?j)
(=> (defined (value ?C ?i ?j))
(= (value ?C ?i ?j)
(- (value ?A ?i ?j))))))))
)

(define-function DETERMINANT (?M) :-> ?det

"Function that returns the determinant of a matrix It has relevant
informations such as if determinant = 0 the the matrix cannot be inverted"

:when (square-matrix ?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)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;  Other Definitions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-function COFACTOR (?M ?i ?j) :-> ?cof

"Function that returns (expt -1 (+ ?i ?j)) * determinant of the matrix less
the row ?i and column ?j"

:iff-def (and (square-matrix ?M)
(< 1 (size ?M))
(defined (value ?M ?i ?j))
(= ?cof (* (expt -1 (+ ?i ?j))
(determinant
(matrix-less-row-and-column ?M ?i ?j))))))

(define-class INVERTIBLE-MATRIX (?M)

"Class of the matrices that can be inverted"

:iff-def (and (square-matrix ?M)
(not (zero-element (determinant ?M))))

:equivalent (and (square-matrix ?M)
(exists ?M-1
(and (square-matrix ?M-1)
(instance-of (* ?M ?M-1) identity-matrix)
(instance-of (* ?M-1 ?M) identity-matrix)))))

(define-function MATRIX-INVERSE (?M) :-> ?M-1
"Function that returns the inversion of a matrix"
:iff-def (and (invertible-matrix ?M)
(invertible-matrix ?M-1)
(instance-of (* ?M ?M-1) identity-matrix)
(instance-of (* ?M-1 ?M) identity-matrix)))

(define-class ORTHOGONAL-MATRIX (?M)

"An orthogonal-matrix is a square-matrix and its transpose is equal to its
inverse."

:iff-def (and (square-matrix ?M)
(= (transpose ?M)
(matrix-inverse ?M))))

(define-function MATRIX-LESS-ROW-AND-COLUMN (?A ?i ?j) :-> ?B

"Function that returns the matrix with a row and a column deleted"

:iff-def (and	(matrix ?A)
(defined (row ?A ?i))
(defined (column ?A ?j))
(matrix ?B)
(= (row-dimension ?B) (- (row-dimension ?A) 1))
(= (column-dimension ?B) (- (column-dimension ?A) 1))
(= ?B (matrix-less-row (matrix-less-column ?A ?j) ?i))))

(define-function MATRIX-LESS-ROW (?A ?i) :-> ?B
"Function that returns the matrix with a row deleted"
:iff-def (and (matrix ?A)
(defined (row ?A ?i))
(matrix ?B)
(= (row-dimension ?B) (- (row-dimension ?A) 1))
(= (column-dimension ?B) (column-dimension ?A))
(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)))))))

(define-function MATRIX-LESS-COLUMN (?A ?i) :-> ?B
"Function that returns the matrix with a column deleted"
:iff-def (and (matrix ?A)
(defined (column ?A ?i))
(matrix ?B)
(= (row-dimension ?B) (row-dimension ?A))
(= (column-dimension ?B) (- (column-dimension ?A) 1))
(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))))))))

```

This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber