报告主题：基于Bernstein多项式的插值的Vasc不等式机械化证明（第一部分: 算法实现的方法与技术）
报 告 人：杨争峰 副教授 （华东师范大学）
报告时间：2019年01月11日（周五）15：00
报告地点：校本部G507
邀 请 人：曾振柄
报告摘要：使用Bernstein基多项式表示初等函数，可以得到截断误差小、次数低的逼近，同时，已经有算法快速计算通过给定样本点的Bernstein多项式。在证明复杂不等式的严重中，由目标函数上的一些网格点构造适当的Bernstein插值多项式，可望将复杂的不等式转化为纯数值操作，从而能够在GPGPU计算机上通过高度并行化的计算证明不等式的正确性，或者在较短时间内找出反例。本报告主要介绍我们在Vasc不等式（n=9）的自动证明中，结合高维空间长方体区域分解、Bernstein多项式插值计算等方法所作的一些研究工作。第二部分是算法实现部分。报告部分内容，来自作者以下论文和工具软件：论文： Min Tang, Zhengfeng Yang and Zhenbing Zeng, Resultant Elimination via Implicitation Equation Interpolation,Journal of System Sciences and Complexity,29(5):1411-1435,2016. 软件： VerifyRealRoots: a MATLAB package for computing real verified solutions of polynomial systems of equations and inequalities.
欢迎教师、学生参加！