線性空間中泛函及對(duì)偶空間在Mizar語言下的實(shí)現(xiàn).pdf

1、目前，隨著計(jì)算機(jī)技術(shù)的發(fā)展，機(jī)器證明已經(jīng)成為一個(gè)非?；钴S的研究領(lǐng)域。人們根據(jù)機(jī)械化方法成功創(chuàng)建了各種機(jī)器語言來編寫程序，并在計(jì)算機(jī)上實(shí)現(xiàn)了數(shù)學(xué)問題的機(jī)器證明。歐洲最常用的機(jī)器證明系統(tǒng)是Mizar語言系統(tǒng)，該系統(tǒng)參與研究者之多，使用者在世界上區(qū)域分布之廣，數(shù)據(jù)庫之大是其它語言系統(tǒng)不能比擬的。
　　 本文介紹了機(jī)器證明及Mizar系統(tǒng)的歷史和研究現(xiàn)狀，對(duì)利用Mizar語言完成數(shù)學(xué)論文和進(jìn)行自動(dòng)推理檢驗(yàn)做了簡(jiǎn)要說明。作者給出了線性空間

2、中泛函在Mizar系統(tǒng)下的若干定義及性質(zhì)；實(shí)現(xiàn)了線性空間中對(duì)偶空間的定義及性質(zhì)。主要工作如下：
　　 1.實(shí)現(xiàn)了線性空間中泛函在Mizar系統(tǒng)下的加法、減法、數(shù)乘等定義，證明了泛函運(yùn)算的基本性質(zhì)定理；
　　 2.定義了線性空間和向量空間之間的模式轉(zhuǎn)換，利用模式轉(zhuǎn)換和向量空間對(duì)偶空間的定義實(shí)現(xiàn)了線性空間對(duì)偶空間的定義，并以定理的形式證明了對(duì)偶空間中元素滿足的條件，討論了對(duì)偶空間的若干性質(zhì)。
　　 以上結(jié)果均通過了M