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

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

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