论文部分内容阅读
介绍我们最近在代数不等式机器证明方面的一些进展.这些进展主要来自于对柱形代数分解算法(cylindrical algebraic decomposition)的改进.
不等式机器证明的一些进展
【摘 要】
：
介绍我们最近在代数不等式机器证明方面的一些进展.这些进展主要来自于对柱形代数分解算法(cylindrical algebraic decomposition)的改进.
【机 构】
：
北京大学
【出 处】
：
第六届全国计算机数学学术会议
【发表日期】
：
2014年10期
其他文献
Linear Invariant Generation for Safety Verification of Nonlinear Systems Using Conservative Approxim
会议
In this paper,a flaw of the Laplace decomposition method is investigated.Based on it a modified Laplace decomposition method is presented,the new algorithm can
会议
本文提出了一种能有效保留模型特征的改进的自适应分层算法.基于模型是否可打印,本文又提出了能有效检测STL文件和CLI文件各种错误的方法.基于Qt和OpenGL,用C++开发了一款分
会议
Computing the Rational Univariate Representations for Zero-dimensional Systems Involving Interval Re
The purpose of this paper is to investigate the rational univariate representations of zero-dimensional systems involving the interval representation.Let F
会议
A commutative ring R is called K-Hermite if,for any rectangular matrix B∈Mm×n(R)(m≤n),there exists Q∈GLn(R) such that BQ is lower trian-gular.This paper inv
会议
本文定义欠定非线性系统的极小二范数解为解向量二范数的极小值点，超定非线性系统的极小二范数解为残差向量二范数的极小值点。本文将方形系统单根的可信验证方法和对称正
Our work focuses on the smooth and continuous convex specular surfaces measurement using a camera and a LCD display.We firstly analyze the geometric characteris
会议
The equivalence of system is an important concept in multidimensional (nD) system,which is closely related to equivalence of multivariate polynomial matrices.Th
会议
杆状病毒是一类有包膜包被的双链DNA病毒,特异性感染节肢动物,是目前已知的广泛应用且对人畜无害的病毒。杆状病毒主要应用于农林害虫防治,作为真核基因表达系统用于外源基因
Analysis-suitable T-splines are a topological restricted subset of T-splines,which are opti-mized to meet the needs for design and analysis.The paper indepe