内容简介
《数学机械化丛书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 电子书 格式