再谈不等式自动发现与判定程序agl2010的改进和应用 被引量：5

1

作者 刘保乾 《汕头大学学报（自然科学版）》 2012年第1期14-23,共10页

对不等式自动发现与判定程序agl2010的功能进行了若干改进,通过15个具体实例演示了程序的强大功能;利用agl算法得到了一类三角形几何不等式最佳系数的估算方法;结合Bottema软件的xprove命令,得到了一种带约束条件不等式自动发现的设计方... 对不等式自动发现与判定程序agl2010的功能进行了若干改进,通过15个具体实例演示了程序的强大功能;利用agl算法得到了一类三角形几何不等式最佳系数的估算方法;结合Bottema软件的xprove命令,得到了一种带约束条件不等式自动发现的设计方案;通过建立数据限制函数,实现了一类变元取值范围受限制条件不等式的自动发现和自动加强,从而拓展了包括Fan Ky不等式在内的一大批不等式类型;最后提出2个有趣的不等式问题. 展开更多

关键词 不等式自动发现 agl算法 agl2010程序 机器证明

下载PDF 职称材料

一类三元对称分式的平方型分拆及其程序实现 被引量：4

2

作者 何灯 《汕头大学学报（自然科学版）》 2011年第1期35-42,共8页

探讨了三元对称分式的平方型分拆,利用待定系数法编写Maple程序fsos实现了分拆,并举例说明了程序在证明不等式中的应用.

关键词 三元对称分式 不等式 平方型分拆 机器证明

下载PDF 职称材料

用反正切函数的级数计算圆周率π的研究 被引量：2

3

作者 王伯年 王宏光 《上海理工大学学报》 EI CAS 北大核心 2005年第3期271-274,共4页

从arctanc=arctana+arctanb和arctanx的级数展开式出发,对圆周率π可以推导出许多计算公式,并可设计出计算软件.基于此软件,可验证现有公式的正确性,找出现有公式的失误,并推导出收敛效率更高的计算公式.

关键词 圆周率 反正切函数 级数计算 Π 计算公式 级数展开式 计算软件 正确性 推导 收敛

下载PDF 职称材料

基于矩形区域剖分的不等式机器证明方法—以Zirakzadeh的一个几何不等式为例 被引量：2

4

作者 曾振柄 张景中 《系统科学与数学》 CSCD 北大核心 2010年第11期1430-1458,共29页

1988年,张景中,陶懋颀用细致的人工估计,用BASIC语言程序在PB700微型计算机上证明了Zirakzadeh于1964年证明的一个几何不等式,其方法是把不等式涉及的变量所在之区域剖分为一系列充分小的矩形,在每个小矩形上用数值方法验证若干三角函... 1988年,张景中,陶懋颀用细致的人工估计,用BASIC语言程序在PB700微型计算机上证明了Zirakzadeh于1964年证明的一个几何不等式,其方法是把不等式涉及的变量所在之区域剖分为一系列充分小的矩形,在每个小矩形上用数值方法验证若干三角函数不等式的正确性.这个工作后来没有发表,将Zirskzadeh不等式转化为一个有3个变元的根式不等式,形如m_1^(/2)+m_2^(/2)+m_3^(/2)≥3m_4^(/2),其变量所在区域为一由6个线性不等式限制形成的多面体P(有14个顶点,21个棱和9个面),先用幂级数展开方法证明讨论的根式不等式在小长方体邻域[-0.1,0.1]~3C P成立,次将这个邻域以外的集合分割成有限多个边长不小于1/1280的小长方体或多面体,在每个小凸体上通过计算函数在顶点的取值和函数偏导数范围证明根式不等式的正确性.文章给出的验证数引理,可根据连续可微函数在长方体或一般凸多面体V的顶点的值,及函数偏导数的绝对值在集合V的上界,证明函数在V上的正定性.文章给出计算多项式在三维空间凸多面体上的最大值和最小值,以及估计根式函数的验证数的机械化方法. 展开更多

关键词 数学机械化 机器证明 Zirakzadeh不等式 矩形剖分 误差分析

原文传递

点集拓扑学之杨忠道定理的一个机械化证明 被引量：1

5

作者 曾振柄 王建林 +1 位作者 杨争峰 小林英恒 《中国科学：数学》 CSCD 北大核心 2021年第1期257-288,共32页

本文给出一种用高阶逻辑自动证明语言Isabelle在计算机中表示拓扑空间中开集、闭集、邻域和导集等基本概念的方法,在此基础上证明点集拓扑学中著名的杨忠道定理,即一拓扑空间的任意单点集的导集为闭集,则其任意子集的导集亦为闭集.

关键词 拓扑空间 开集 闭集 导集 杨忠道定理 机器证明

原文传递

质点法机器证明视角下的近世几何研究 被引量：1

6

作者 李涛 邹宇 《计算机应用》 CSCD 北大核心 2012年第11期3057-3061,共5页

优化并发展了质点法机器证明算法的核心程序,用Mathematica创建了新的几何定理证明器。拓展了机器证明的研究范畴,首次实现了近世几何的机器证明,且可读性令人满意。在该证明器的帮助下,发现了一些新的近世几何性质,深化了近世几何的研... 优化并发展了质点法机器证明算法的核心程序,用Mathematica创建了新的几何定理证明器。拓展了机器证明的研究范畴,首次实现了近世几何的机器证明,且可读性令人满意。在该证明器的帮助下,发现了一些新的近世几何性质,深化了近世几何的研究成果,并对已有的近世几何研究成果提出一些意见。 展开更多

关键词 质点法 机器证明 Mathematica证明器 近世几何

下载PDF 职称材料

关于对称多项式的构造及其应用 被引量：1

7

作者 何灯 《汕头大学学报（自然科学版）》 2010年第4期1-7,25,共8页

通过构造对称式和轮换对称式的一般表示式,借助于Maple应用程序,研究了3元到15元的对称多项式的缺项多项式、轮换对称代换缺项多项式、Si类对称多项式及Si类差分代换缺项多项式的通式构造,并对多元多项式的平方分拆进行了探讨.

关键词 对称多项式 缺项多项式 Si类多项式 平方分拆 机器证明

下载PDF 职称材料

定理机器证明与传统数学观

8

作者 骆祖英 《浙江师大学报（自然科学版）》 1996年第4期1-4,共4页

本文从回顾历史上费马猜想和四色猜想被证明为定理的不同方法入手，阐发了机器证明的发展历史和吴方法的思想渊源，论述了计算机对传统数学观的冲击与挑战。

关键词 定理 机器证明 数学观 费马猜想 四色猜想

下载PDF 职称材料

基于Coq的有标集族相关定理的机器证明

9

作者 刘佳 吕红伟 +1 位作者 付尧顺 郁文生 《伊犁师范学院学报（自然科学版）》 2020年第2期13-22,共10页

基于计算机证明辅助工具Coq,参考“公理化集合论”形式化系统,实现朴素集合论形式化系统,并在此基础上给出有标集族及其交和并的形式化,完成有标集族相关定理的Coq描述及机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,... 基于计算机证明辅助工具Coq,参考“公理化集合论”形式化系统,实现朴素集合论形式化系统,并在此基础上给出有标集族及其交和并的形式化,完成有标集族相关定理的Coq描述及机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了Coq的规范、严谨、可靠.为构建完整的点集拓扑理论打下基础,在此系统下,有望实现拓扑空间相关性质的形式化系统. 展开更多

关键词 COQ 机器证明 公理化集合论 有标集族

下载PDF 职称材料

重心坐标法证明几何定理

10

作者 沈效良 《中国西部科技》 2009年第24期79-80,共2页

众所周知,在欧氏平面中,如取定一个标架后,可以用坐标的计算来做几何证明,类似地考虑,我们如取定一个三角形(它相当于一个标架)可以引入重心坐标。自然地可以用重心坐标来做几何。三角形是几何中最稳定的,而且很美。本文以重心坐标的方... 众所周知,在欧氏平面中,如取定一个标架后,可以用坐标的计算来做几何证明,类似地考虑,我们如取定一个三角形(它相当于一个标架)可以引入重心坐标。自然地可以用重心坐标来做几何。三角形是几何中最稳定的,而且很美。本文以重心坐标的方法来证明几道初等几何中的难题,以比较其与其它坐标的优缺点,并试图找出一个完善的理论,能解决所有的几何问题,这对机械化证明也许是有帮助的。 展开更多

关键词 几何 重心坐标 机器证明 笛卡儿坐标

下载PDF 职称材料

质点几何定理证明的机器实现

11

作者 苏贺靓 江建国 高华 《科技视界》 2015年第15期96-97,168,共3页

本文针对质点法生成的目标关系式的过程不简明,缺少明显几何意义的问题,提出了一种具有较高可读性算法的几何定理证明器MMP.首先,直接从消点公式推导目标关系式,该方法不再使用质点坐标而直接对质点进行运算;其次,利用三个模块架构证明... 本文针对质点法生成的目标关系式的过程不简明,缺少明显几何意义的问题,提出了一种具有较高可读性算法的几何定理证明器MMP.首先,直接从消点公式推导目标关系式,该方法不再使用质点坐标而直接对质点进行运算;其次,利用三个模块架构证明器,形成了具有完全性的消点过程;最后,利用待定系数法判定结论语句.由于可以对点直接进行运算,该证明器的消点过程比原有质点法具有明显的几何意义和较高运算效率. 展开更多

关键词 质点几何 证明器 消点法 机器证明 自动推理

下载PDF 职称材料

仿射质点几何的可读机器证明 被引量：8

12

作者 邹宇 郑焕 张景中 《计算机应用》 CSCD 北大核心 2010年第7期1899-1901,1912,共4页

讨论并发展了能自动证明几何定理的质点几何方法,建立了能处理希尔伯特交点类命题的仿射几何机器证明算法,并实现为Maple程序。对上百个非平凡命题运行的结果显示,这种方法不仅效率高,多数证明的可读性也令人满意。

关键词 质点几何 可读机器证明 希尔伯特交点类几何命题

下载PDF 职称材料

几何定理可读证明的自动生成 被引量：22

13

作者 张景中 杨路 +1 位作者 高小山 周咸青 《计算机学报》 EI CSCD 北大核心 1995年第5期380-393,共14页

用计算机能生成几何定理的易为人们理解的证明吗？这个几十年来进展很小的难题，自１９９２年以来有了突破性进展．对于一大类欧氏几何命题──构造性几何命题，已有了相当有效的算法．基于此算法所编制的程序，已证明了５００多条非平... 用计算机能生成几何定理的易为人们理解的证明吗？这个几十年来进展很小的难题，自１９９２年以来有了突破性进展．对于一大类欧氏几何命题──构造性几何命题，已有了相当有效的算法．基于此算法所编制的程序，已证明了５００多条非平凡的几何命题．对其中大多数命题，机器自动生成的证明是简明而易于理解的．本文是对这一领域近三年来取得的进展的综述．包括了在非欧几何可读证明方面的最新成果． 展开更多

关键词 可读机器证明 几何定理 计算机

下载PDF 职称材料