数字技术与应用
·软件设计开发·
矩阵的证明及运算在Mizar系统下的实现
果希来刘玲玲姜西春
(青岛科技大学山东青岛266061)
摘要：本文在计算机上利用有限序列的复合映给出了矩降在Mizar系统下的定义，实现了可逆矩阵，对称和反对称矩阵，桐似矩阵，合同矩降等特殊矩阵的定又，给出了与上述矩阵有关的一些定理的计算机证明，并实现了矩降的初等变换及相关运算。
关键词：矩阵Mizar
初等变换
中图分类号：TP312
文献标识码：A
1.引言
由于所研究的数学问题越来越深入，越来越困难，数学机械化成为一种趋势，计算机技术的高速发展加速了数学机械化的进程。各种自动推理与证明系统在实践中日益完善，目前，应用最广泛的是Mizar语言系统。本文将详细介绍Mizar系统下各种矩阵及其性质的实现。
本文中的所有定理.定义的实现过程都已经过Mizar检验系统的验证，并收录到Mi zar数据库中。为了避免篇幅过长，文中举例证明了几个定理、定义，其余的定理、定义的证明过程省略(所有过程可在Mizar数据库中查询)。
2、矩阵的定义及性质在Mizar系统下的实现
在Mizar数据库中，有限序列是通过关系定义的一个特殊函数，其定义城为[1,2,,川]，那么它就有n个值，下面先利
用有限序列给出表格的定义： Definitionl:
let f be FinSequence; attr f is tabular means
ex n being Nat st (for x st x in rn gfexs
being FinSequence st s=x & len s = n,)
end
即每个元素都是相同维数的有限序列的有限序列称为表格。矩阵可以用表格定义为：
Definition2 let D be set,
mode Matrix of D is tabular FinSeq uenceof D,
end,
其中D*是D上所有非空有限序列的集合。
利用矩阵的定义，D上mxn矩阵的定
114
数字技术与应用万方数据
义如下：
Definition3: let D,let m,n;
文章编号：1007-9416(2011)03-0114-03
assume p in mg M,
then p = n /> a by A2,TARSKI: def 1,
mode Matrix of m,n,D -> Matrix o fDmeans
len it = m & for p st p in mg it h olds len p = n;
existence-proof
()
reconsider ml=m,nl=n as Element o
f
NAT
ORDINALI:def aq
3..+.....
set a = the Element of D,
**.. (2)
reconsider d= nl I> a as Element o f D+ by FINSEQ_1:def 11,
reconsider M= m1 (> d as FinSeq uence of D+
exnbeElementofNATstforxst u d al d= x s d xa B u x
proof
enos se d apso ce of D;
take nl; let x; assume
Al.x in mg M,... take ps
(3)
19
hence thesis by A1,CARD_1:def 13,
TARSKI;def 1, end;
then reconsider M as Matrix of D b y Th9,
take M,
thus len M = m by CARD_1:def 1
3,
let p:
A2: mg M c= (n /> a) by FUNC OP_1:19，
Digital technology and application
hence thesis by CARD_1:def 13
end, end,
这种模式(mod)定义需要证明存在性如处(U)所示；by后表示该命题成立所需要的依据，如(2)所示；定理中后面还要引用的命题前面要加标号如(3)处所示。
3、矩阵的性质及几类特殊矩阵在 Mizar系统下的实现
3.1可交换矩阵，可逆矩阵，对称矩阵、正交矩阵
定义：M,，M,为n阶方阵，若M,M，
=M,M,，则称M,与M,是可交换的。 Definition4:
let n be Nat, K be Field, M1,M2 b e Matrix of n,K,
pred M1 commutes_with M2 means M1 * M2 = M2 * M1,
reflexivity symmetry end,
定义：M,，M,为n阶方阵，若M,M， =M,M,,且M,M,=E，则称M,与M,是互逆3
定义方阵M称为对称的，如果M =M。
Definition6：
let n be Nat, K be Field, let M1 be Matrix of n,K, attr M1 is symmetric means
M1@=Ml end
对称矩阵是通过矩阵的转置定义的，反对称矩阵可以用类似的方法定义，此处略。定义：方阵M称为正交的，如果M是可逆的,且MT=M-I。