關(guān)于反對(duì)稱反循環(huán)矩陣的幾個(gè)性質(zhì)及循環(huán)矩陣在Mizar系統(tǒng)中的實(shí)現(xiàn).pdf

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

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

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