-
题名Tarski模型外的一类机器可判定问题
被引量：3
- 1
-
-
作者
杨路
姚勇
冯勇
-
机构
中国科学院成都计算机应用研究所
-
出处
《中国科学（A辑）》
CSCD
北大核心
2007年第5期513-522,共10页
-
基金
国家重点基础研究发展规划基金资助项目(批准号:2004CB318003)
-
文摘
利用对称多项式的降维方法和证明代数不等式的胞腔分解方法,给出了一个实用的算法,用于判定一类变元个数也是变量的多项式正性命题．这是一类在Tarski模型外的机器可判定问题．在Maple平台上,根据该算法设计的程序nprove,可以快速实现判定目标．
-
关键词
对称多项式不等式
胞腔分解
Tarski模型
机器可判定问题
-
分类号
O174.14
[理学—数学]
-
-
题名计算机怎样证明几何不等式
- 2
-
-
作者
杨路
-
机构
广州大学计算机教育软件研究所
-
出处
《广州大学学报（自然科学版）》
CAS
2004年第2期97-106,179,共11页
-
基金
国家973计划(NKBRSF-G1998030602)
中国科学院知识创新工程资助项目
-
文摘
阐述了一个基于胞腔分解的不等式机器证明软件的原理、算法和使用方法,这一用Maple语言编写的程序能有效地处理含有根式的不等式型定理,对于Bottema等所著《几何不等式》一书中的大部分不等式定理的验证尤其高效.对一类代数结构较为简单的几何不等式,能令计算机自动生成和输出用自然语言写出的证明.
-
关键词
自动证明
几何不等式
构造性几何定理
半代数系统
胞腔分解
-
Keywords
automated proving
geometric inequality
constructive geometric theorem
semi-algebraic system
cell decomposition
-
分类号
TP3
[自动化与计算机技术—计算机科学与技术]
-
-
题名一类三角形几何不等式的自动证明
被引量：4
- 3
-
-
作者
陈世平
刘忠
-
机构
四川省商贸学校
中国民航飞行学院德阳校区
四川建筑职业技术学院
-
出处
《计算机应用研究》
CSCD
北大核心
2012年第5期1732-1736,共5页
-
文摘
讨论了一类只含三角函数的三角形几何不等式的自动证明问题。运用代数方法将其有理化,在不新增加根式的条件下将问题转换为一个二元多项式不等式的证明,设计的基于胞腔分解和实根分离的算法实现了二元多项式不等式的自动证明,输出的证明过程可以手工验证或借助一些数学软件进行理解。实验表明上述算法对一大批具有相当难度,特别是关于三角函数的几何不等式十分高效,并且能够解决三角形内角的任意有理倍数函数的不等式机器证明问题。
-
关键词
几何不等式
可读证明
有理化
实根分离
胞腔分解
-
Keywords
geometric inequalities
readable proof
rationalization
real root isolation
cell decomposition
-
分类号
TP3
[自动化与计算机技术—计算机科学与技术]
-
