內容簡介
《數學機械化叢書11:不等式機器證明與自動發現》主要介紹作者及其閤作者近十年來在不等式機器證明與自動發現方麵的工作,兼顧經典結果和方法,全書共分7章,分彆介紹和論述多項式的僞除與結式、相對單純分解、多項式的實根、常係數半代數係統的實解隔離、參係數半代數係統的實解分類、不等式機器證明的降維算法與BOTTEMA程序以及不等式的明證.除第1章及第3章、第7章的部分內容外,餘皆作者及閤作者的工作.附錄介紹瞭子結式理論和柱形代數分解算法,還包括瞭對作者自編軟件包BO‘兀EMA的使用說明.
《數學機械化叢書11:不等式機器證明與自動發現》可作為高等院校、科研機構數學或計算機科學方嚮研究生的教材,也可作為相關專業研究人員和工程技術人員的參考書.
內頁插圖
目錄
第1章 多項式的僞除與結式
1.1 僞除
1.2 結式
1.3 子結式
1.4 三角列
第2章 相對單純分解
2.1 多項式關於三角列的結式
2.2 多項式關於三角列的僞除
2.3 相對單純分解算法
2.4 三角列的相關性
2.5 三角化的半代數係統
2.6 -般的半代數係統
第3章 多項式的實根
3.1 經典結果
3.2 多項式的判彆係統
3.3 判彆定理的證明
3.4 判彆矩陣的某些性質
3.5 多項式的實根隔離
第4章 常係數半代數係統的實解隔離
4.1 單調性與第一算法
4.2 若乾實例
4.3 區間算術
4.4 第二算法
4.5 討論
第5章 參係數半代數係統的實解分類
5.1 邊界多項式和判彆多項式
5.2 基本算法
5.3 正維數與超定情形
5.4 DISCOVERER與例子
5.5 幾何不等式的自動發現
5.6 生物係統穩定性的代數分析
5.7 混成係統的可達性
第6章 不等式機器證明的降維算法與BOTTEMA程序
6.1 半代數係統的不相容性
6.2 基本定義
6.3 降維算法
6.4 關於三角形的不等式
6.5 BOTTEMA程序及若乾實例
6.6 全局優化的符號算法與有限核原理
6.7 藉助BOTTEMA模擬數學歸納法
6.8 Tarski模型外的一類機器可判定問題
第7章 不等式的明證
7.1 平方和錶示
7.2 Schur分拆
7.3 差分代換
參考文獻
附錄A 子結式
A.1 Habicht定理
A.2 子結式鏈定理
A.3 子結式多項式餘式序列
附錄B 柱形代數分解算法
B.1 基本概念
B.2 基本算法
附錄C BOTTEMA簡易使用指南
C.1 如何安裝和運行BOTTEMA
C.2 關於三角形中幾何不變量的約定記號列錶(可擴充)
C.3 證明不等式型定理的主要指令及其例解
C.4 關於全局優化的主要指令及其例解
附錄D 六次多項式根的分類
索引
前言/序言
自古以來,物理量之間大小的比較為現實世界之必需,這導緻瞭數學不等式的産生和發展.迄今,不等式的重要應用已貫穿於當代科學技術和工程領域的多個學科分支,
不等式在數學中從來就不是一個二級或三級的相對獨立的學科,而是“哪裏不平哪裏有我”.關於不等式的係統研究應該是近八十年之內的事情。1929年,Bohr嚮Hardy抱怨說:“所有的分析學傢都要花一半時間從文獻中搜尋他們需用然而未能證明的不等式.”5年之後,Hardy,Littlewood和P61ya齣版瞭係統研究不等式的經典名著“Inequalities”,1952年發行瞭第二版,該書帶有Hardy作品中一以貫之的漂亮的代數風格;關於不等式的第二本重要著作當推1965年Beckenbach和Bellman的與上麵同名的專著,後者的部分內容與前者重疊,但包含瞭許多較現代的題材和方法以及較多的應用;第三本應該是Mitrinovi6於1970年齣版的“AnalyticInequalities”,這是一部近乎詞典式的工具書,包含瞭從彆處不易獲得的若乾材料。
以上以及同類的工作,雖然提供瞭不等式的大量研究成果和多種論證方法,卻不能適應數學機械化和推理自動化的需要,由於沒有建立強有力的判定算法,不能對一些常見的不等式問題類作整體的解決,更不可能對大量的在綫問題作實時判定.Hardy在他的書齣版5年後被問及:該書是否對Bohr提到的情況有所改善?Hardy迴答說,從這本書裏似乎從來都找不到我所需要的東西。
本書主題是如何用計算機證明和發現代數不等式,著重研究實用的算法和程序,固然不同於上麵提到的不等式經典,與國內外闡述實代數或實代數幾何的理論性專著也有明顯的區彆,但為瞭理論上做到自成體係以方便研讀,必須補充一些基礎知識包括作者及其閤作者的若乾有關的理論工作作為鋪墊,這部分內容構成本書的前兩章和附錄A、附錄B。
代數不等式問題的本質是多項式或多項式組實零點的存在和分類問題,所以在接下來的三章討論瞭多項式的實根、常係數半代數係統的實解隔離和參係數半代數係統的實解分類,其中第5章介紹瞭實現參係數半代數係統的實解分類的程序DISCOVERER,並水到渠成地闡述瞭該程序自動發現不等式型定理的功能。
第6章介紹代數不等式機器證明的降維算法以及對應的程序BOTTEMA,這是一個簡便快速的不等式證明器,可以直接處理帶多重根式的不等式.最後兩節討論如何嘗試將本章的算法和程序應用於“高等問題”,即超齣Tarski所界定的“初等”範圍的問題.譬如,不等式中變量的個數是一個不確定的正整數n.讀者會發現這部分內容是富有吸引力的,雖然探索可以說是剛剛開始。
第7章介紹幾項探索式研究的進展,其中包括Hilbert第17問題的構造性研究,這些算法雖不完備,但在實際中常能解決許多原本束手無策的問題,特彆是這些方法産生的證明是可讀性很強的“明記”(certificate),它無需專傢“審稿”,普通讀者即可”核對“無誤。
由於本書讀者包括不同的群體,對理論部分暫時無暇顧及,但對不等式機器證明的實用算法和程序有興趣的讀者可以直接閱讀第6章、第7章和附錄C.俟機再讀其餘部分,
本書係統地介紹作者及其閤作者近十年來在不等式機器證明與自動發現方麵的工作,除第1章及第3章、第7章部分內容外,餘皆作者及閤作者的工作。
值此書稿完成之際,作者衷心感謝吳文俊先生、鬍國定先生和吳文達先生多年的教誨和幫助。
深切懷念已經離去的程民德先生。
衷心感謝十年來從多方麵對作者幫助和支持的親人、同事和朋友們。
衷心感謝國傢重點基礎研究發展計劃”數學機械化方法及其在信息技術中的應用“項目的鼎力支持,使本書得以順利齣版。
數學機械化叢書11:不等式機器證明與自動發現 下載 mobi epub pdf txt 電子書 格式