一元函數(shù)高階導(dǎo)數(shù)在Mizar語言系統(tǒng)下的實現(xiàn)研究.pdf

1、數(shù)學(xué)問題的計算機證明也稱數(shù)學(xué)機械化，是指用計算機證明、推理計算數(shù)學(xué)問題。Mizar語言系統(tǒng)是由波蘭華沙大學(xué)的AndrzejTrybulec教授為首的數(shù)學(xué)家和計算機專家在上世紀(jì)八十年代開創(chuàng)的集邏輯證明、校驗、排版功能于一體的計算機語言系統(tǒng)。該系統(tǒng)如今擁有自己的數(shù)據(jù)庫MML，其中收錄了幾乎涵蓋了數(shù)學(xué)各個分支的1000多篇數(shù)學(xué)論文，并且還解決了像連續(xù)格的證明、Jordan曲線及Brouwer不動點等定理，這類人們用手無法計算和證明的復(fù)雜問題。

2、同時，它在自動化控制、聲音和圖像識別等研究領(lǐng)域也有著廣泛的應(yīng)用。 本文首先介紹了Mizar語言系統(tǒng)的發(fā)展歷史，其次給出了在該系統(tǒng)下證明和自動校驗數(shù)學(xué)命題的方法，在此基礎(chǔ)上針對一元函數(shù)高階導(dǎo)數(shù)的不同問題，給出了相應(yīng)的Mizar算法。作者的主要工作如下： 1.在Mizar語言系統(tǒng)下給出了幾類一元函數(shù)高階導(dǎo)數(shù)公式的實現(xiàn)方法； 2.實現(xiàn)了廣義指數(shù)函數(shù)的Mizar語言定義方法，證明了其復(fù)合函數(shù)的可微性定理并推導(dǎo)了其高階導(dǎo)數(shù)