向量函數(shù)、微分及偏微分基本公式的計(jì)算機(jī)證明.pdf

1、Mizar系統(tǒng)是由波蘭華沙大學(xué)的Andrzej Trybulec教授于二十世紀(jì)七十年代開(kāi)創(chuàng)的集邏輯證明、推理演繹、校驗(yàn)排版、復(fù)雜計(jì)算、科研教學(xué)功能于一體的形式化系統(tǒng)，同時(shí)在自動(dòng)化控制、聲音和圖像識(shí)別等研究領(lǐng)域有著廣泛的應(yīng)用。如今該系統(tǒng)擁有世界上最大的數(shù)據(jù)庫(kù)MML。
　　 本文首先介紹Mizar系統(tǒng)的發(fā)展歷史，其次簡(jiǎn)要說(shuō)明Mizar論文的基本結(jié)構(gòu)。利用Mizar語(yǔ)言系統(tǒng)實(shí)現(xiàn)了向量函數(shù)的表示，討論其若干性質(zhì)。給出向量函數(shù)微分及偏微分

2、算子的定義，并在計(jì)算機(jī)上推導(dǎo)證明了若干基本公式。
　　 本文主要從以下幾個(gè)方面在Mizar系統(tǒng)中進(jìn)行研究：
　　 1.基于Mizar中對(duì)于度量空間和歐氏空間定義的理解，給出了向量函數(shù)的Mizar表示，在此基礎(chǔ)上進(jìn)而討論了向量函數(shù)的有關(guān)性質(zhì)。
　　 2.在Mizar系統(tǒng)下，借助實(shí)函數(shù)可微性的定義，給出向量函數(shù)微分定義的Mizar形式，并證明了向量函數(shù)微分的基本公式。
　　 3.利用Mizar系統(tǒng)中n維賦范線