關于反對稱反循環(huán)矩陣的幾個性質及循環(huán)矩陣在Mizar系統中的實現.pdf

1、循環(huán)矩陣屬于Teoplitz矩陣類。一般n階Teoplitz矩陣的特殊性在于它僅有2n-1個元素并且位于每一條平行于主對角線的直線上的元素都相同，而循環(huán)矩陣除了具有Teoplitz矩陣的一般性質外，還具有更加特殊的性質，如：一般的n階循環(huán)矩陣只含有n個元素、它的任意行可以通過對矩陣的第一行進行置換得到等?；谘h(huán)矩陣類的良好性質和結構，對它進行研究會得到很多有意義的結果。 Mizar系統是15個著名的數學定理證明系統之一，它在波

2、蘭Plock科學協會的AndrzejTrybulec教授的領導下己經發(fā)展了近30年，目前Mizar系統已經形成了較完備的數學知識處理的形式化系統，它所包含的數學知識幾乎涵蓋了數學的每一個分支，但是相對于龐大的數學知識庫，很多領域仍然需要我們進一步的開發(fā)和研究。 文中首先敘述了循環(huán)矩陣的性質以及其相關的發(fā)展，包括循環(huán)矩陣，反循環(huán)矩陣，對稱循環(huán)矩陣等，然后結合這些知識給出反對稱反循環(huán)矩陣的相關的概念及性質。最后，利用有限序列在Miz

3、ar系統中給出了關于一般循環(huán)矩陣的幾個定義，從而在Mizar系統中給出了關于一般循環(huán)矩陣的一些基本性質的證明。 本文共分三部分： 第一部分：給出相關的預備知識，主要是循環(huán)矩陣研究的國內外進展、文中用到的循環(huán)矩陣的基本概念、性質以及對Mizar系統的介紹。 第二部分：綜述循環(huán)矩陣的有關性質及證明，給出反對稱反循環(huán)矩陣的概念及相關的性質。 第三部分：利用有限序列將一般循環(huán)矩陣在Mizar系統進行實現，豐富Mi