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

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

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

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