广义循环矩阵的性质及循环矩阵在Mizar系统中的实现

广义循环矩阵的性质及循环矩阵在Mizar系统中的实现

论文摘要

循环矩阵属于Teoplitz矩阵类。一般n阶Teoplitz矩阵的特殊性在于它仅有2n-1个元素并且位于每一条平行于主对角线的直线上的元素都相同,而循环矩阵除了具有Teoplitz矩阵的一般性质外,还具有更加特殊的性质,如:一般的n阶循环矩阵只含有n个元素、它的任意行可以通过对矩阵的第一行进行置换得到等。基于循环矩阵类的良好性质和结构,对它进行研究将会得到很多有意义的结果。Mizar系统是15个著名的数学定理证明系统之一,它在波兰Plock科学协会的Andrzej Trybulec教授的领导下已经发展了近30年,目前Mizar系统已经形成了较完备的数学知识处理的形式化系统,它所包含的数学知识几乎涵盖了数学的每一个分支,但是相对于庞大的数学知识库,很多领域仍然需要我们进一步的开发和研究。文中首先利用广义范德蒙矩阵讨论了广义循环矩阵的准对角化问题,并由所得到的结果,获得了广义循环矩阵的一些相关性质,进而讨论了几种广义循环矩阵求逆的算法。最后,利用有限序列在Mizar系统中给出了关于一般循环矩阵的几个定义,从而在Mizar系统中给出了关于一般循环矩阵的一些基本性质的证明。本文共分三章:第一章:给出相关的预备知识,主要是循环矩阵研究的国内外进展、文中用到的循环矩阵的基本概念、性质以及对Mizar系统的介绍。第二章:利用广义范德蒙矩阵对广义循环矩阵进行对角化,并对几种广义循环矩阵求逆的方法进行比较。第三章:利用有限序列将一般循环矩阵在Mizar系统进行实现,丰富Mizar数据库的内容。

论文目录

  • 摘要
  • ABSTRACT
  • 1、绪论及预备知识
  • 1.1 循环矩阵的发展和基本性质
  • 1.2 矩阵的Kronecker积
  • 1.3 Mizar系统介绍
  • 1.4 本文内容及安排
  • 2、广义循环矩阵及其性质
  • 2.1 引言
  • 2.2 广义范德蒙矩阵的行列式
  • 2.3 广义循环矩阵的准对角化
  • 2.4 广义循环矩阵的几种求逆方法
  • 2.4.1 利用行列式求逆
  • 2.4.2 利用矩阵分块对循环矩阵求逆
  • 2.4.3 特殊的广义循环矩阵的求逆公式
  • 2.4.4 (m,n)型二重循环矩阵逆的初等解法
  • 2.4.5 利用广义循环矩阵的准对角化给出循环矩阵的逆
  • 3、循环矩阵在MIZAR系统中的实现
  • 3.1 引言
  • 3.1.1 Mizar数据库
  • 3.1.2 Mizar系统
  • 3.1.3 Mizar文章的结构
  • 3.1.4 Mizar文章的书写过程
  • 3.1.5 Mizar文章的提交、收录及发表
  • 3.2 循环矩阵在Mizar系统中的实现
  • 3.2.1 MATRIX14中环境部的设置
  • 3.2.2 MATRIX14中变量的设置
  • 3.2.3 MATRIX14中的定义以及证明
  • 3.2.4 几类特殊的循环矩阵
  • 3.2.5 循环矩阵的一般定理
  • 3.2.6 MATRIX14的最后检查和优化
  • 结束语
  • 参考文献
  • 致谢
  • 攻读学位期间参与的科研项目
  • 攻读学位期间发表(完成)的学术论文目录
  • 相关论文文献

    标签:;  ;  ;  ;  ;  

    广义循环矩阵的性质及循环矩阵在Mizar系统中的实现
    下载Doc文档

    猜你喜欢