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