關(guān)于我們
書(shū)單推薦
新書(shū)推薦

分析基礎(chǔ)機(jī)器證明系統(tǒng)

分析基礎(chǔ)機(jī)器證明系統(tǒng)

定  價(jià):198 元

叢書(shū)名:數(shù)學(xué)機(jī)械化叢書(shū)

        

  • 作者:郁文生
  • 出版時(shí)間:2022/1/1
  • ISBN:9787030706713
  • 出 版 社:科學(xué)出版社
  • 中圖法分類(lèi):O171 
  • 頁(yè)碼:420
  • 紙張:
  • 版次:31
  • 開(kāi)本:16
9
7
7
8
0
7
6
0
7
3
1
0
3

讀者對(duì)象:人工智能、數(shù)學(xué)與信息科學(xué)相關(guān)領(lǐng)域(計(jì)算機(jī)、控制、電子與通信等) 研究人員、研究生、高年級(jí)本科生等

本書(shū)利用交互式定理證明工具Coq,在樸素集合論的基礎(chǔ)上,從Peano五條公設(shè)出發(fā),完整實(shí)現(xiàn)Landau著名的《分析基礎(chǔ)》中實(shí)數(shù)理論的形式化系統(tǒng),包括對(duì)該專(zhuān)著中全部5個(gè)公設(shè)、73條定義和301個(gè)定理Coq描述,其中依次構(gòu)造了自然數(shù)、分?jǐn)?shù)、分割、實(shí)數(shù)和復(fù)數(shù),并建立了Dedekind實(shí)數(shù)完備性定理,從而迅速且自然地給出數(shù)學(xué)分析的堅(jiān)實(shí)基礎(chǔ).在分析基礎(chǔ)形式化系統(tǒng)下,給出Dedekind實(shí)數(shù)完備性定理與它的幾個(gè)著名等價(jià)命題間等價(jià)性的機(jī)器證明,這些命題包括確界存在定理、單調(diào)有界定理、Cauchy-Cantor閉區(qū)間套定理、Heine-Borel-Lebesgue有限覆蓋定理、Bolzano-Weierstrass聚點(diǎn)原理、Bolzano-Weierstrass列緊性定理及Bolzano-Cauchy收斂準(zhǔn)則等,基于實(shí)數(shù)的完備性定理,作為應(yīng)用,進(jìn)一步給出閉區(qū)間上連續(xù)函數(shù)的重要性質(zhì)——有界性定理、最值定理、介值定理、一致連續(xù)性定理——的機(jī)器證明.另外,還給出張景中院士提出的第三代微積分——不用極限的微積分——的形式化系統(tǒng)實(shí)現(xiàn).在我們開(kāi)發(fā)的系統(tǒng)中,全部定理無(wú)例外地給出Coq的機(jī)器證明代碼,所有形式化過(guò)程已被Coq驗(yàn)證,并在計(jì)算機(jī)上運(yùn)行通過(guò),體現(xiàn)了基于Coq的數(shù)學(xué)定理機(jī)器證明具有可讀性和交互性的特點(diǎn),其證明過(guò)程規(guī)范、嚴(yán)謹(jǐn)、可靠.該系統(tǒng)可方便地應(yīng)用于數(shù)學(xué)分析相關(guān)理論的形式化構(gòu)建.

更多科學(xué)出版社服務(wù),請(qǐng)掃碼獲取。
 你還可能感興趣
 我要評(píng)論
您的姓名   驗(yàn)證碼: 圖片看不清?點(diǎn)擊重新得到驗(yàn)證碼
留言?xún)?nèi)容