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

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

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