中国科学院数学与系统科学研究院期刊网

2009年, 第29卷, 第9期　刊出日期：2009-09-25
  

  • 全选
    |
    论文
  • 几何定理机器证明三十年
    张景中;李永彬
    系统科学与数学. 2009, 29(9): 1155-1168. https://doi.org/10.12341/jssms08447
    摘要 ( ) PDF全文 ( )   可视化   收藏
    由于传统的兴趣和多种原因,几何定理的机器证明在自动推理的研究中占有重要的地位.自吴法发表至今30年,几何定理机器证明的研究和实践有了很大的进展.对无序几何命题而言,代数方法、数值方法均能有效地判定其真假,面积法(消点法)、搜索法更能生成其可读的证明.几何不等式机器证明的研究,由于多项式完全判别系统的建立,也有了突破.研究领域已由机器证明扩展为包括几何作图在内的一般几何问题的机器求解,并有了实际的应用.
  • 差分代换矩阵与多项式的非负性判定
    杨路;姚勇
    系统科学与数学. 2009, 29(9): 1169-1177. https://doi.org/10.12341/jssms08448
    摘要 ( ) PDF全文 ( )   可视化   收藏
    主要分析了差分代换矩阵的基本性质,证明了存在有限个差分代换矩阵的乘积可以将单位点
    $(1,0,\cdots,0)$变换到指定的非负(本原)整点.利用这一结果可以导出${R^n_+}$上判定半正定型的充要条件.根据此充要条件建立的算法(TSDS)可能不停机,针对不停机的情况,再给出一些判定半正定型的充分条件.
  • 曲面上一种等距不变量的构造
    胡平;曹伟国;李涛涛;李华;林宗楷
    系统科学与数学. 2009, 29(9): 1178-1188. https://doi.org/10.12341/jssms08449
    摘要 ( ) PDF全文 ( )   可视化   收藏
    提出一种基于曲面内蕴度量的等距变换不变量构造方法.通过不变几何基元构造不变核,再对不变核进行多重积分,得到曲面上的等距不变量.这种不变量完全基于曲面的内在属性,有直观的几何解释,并且不受数量约束.实验表明,它对于描述曲面的等距变换,如不同表情的同一人脸、不同姿态的同一人体运动等具有潜在应用意义.
  • 几何代数在定理证明中的消元与化简算法
    曹源昊;李洪波
    系统科学与数学. 2009, 29(9): 1189-1199. https://doi.org/10.12341/jssms08450
    摘要 ( ) PDF全文 ( )   可视化   收藏
    在符号计算中,最困难的一个地方是中间计算过程的表达式快速膨胀.基于不变量代数的符号几何计算为解决这个困难提供了可能.比如,利用零几何代数证明欧氏几何定理时,就可以给出很短的证明,甚至是单项式证明.中间的证明过程里有很多地方涉及到消元,展开,化简等问题.从程序实现的角度出发,在充分利用零几何代数计算特点的基础上,给出用于机器证明的消元、化简算法.
  • Yang-Mills规范场的存在性、可解性(一)
    石赫
    系统科学与数学. 2009, 29(9): 1200-1210. https://doi.org/10.12341/jssms08452
    摘要 ( ) PDF全文 ( )   可视化   收藏
    应用数学机械化方法研究欧氏空间中$SU(2)$ Yang-Mills规范场的存在性问题.首先对YM--方程的结构进行了讨论,说明YM--方程由它的奇部份和偶部份联立组成.对于YM--方程构造了一类线性微分变换,称之为$SU(2)$规范场的示性变换.经示性变换,将非线性的YM--方程的奇部份变为一组Laplace方程,实现了$SU(2)$规范场方程的线性化.从而证明了$SU(2)$规范场存在3个独立的Yang-Mills规范场.
  • 三级四阶显式辛R-K-N格式的完全构造
    徐松;侯晓荣
    系统科学与数学. 2009, 29(9): 1211-1221. https://doi.org/10.12341/jssms08454
    摘要 ( ) PDF全文 ( )   可视化   收藏
    s级p阶辛Runge-Kutta-Nystr\"om(R-K-N)方法的一种充要条件是用关于参数的非线性方程组来表示的,辛R-K-N格式的构造问题因而转化为该方程组的求解问题. 在一些特殊的限定条件下, 已有该方程组在s=3,p=4时的两组解,即得到了两个三级四阶显式辛格式. 对于s=3,p=4情形,基于吴方法,利用计算机代数系统Maple及软件包wsolve给出了对应的非线性方程组的全部解, 这样就构造了所有的三级四阶显式辛R-K-N格式, 并证明了三级四阶显式辛R-K-N方法所满足的
    条件方程有冗余. 数值实验结果显示出新的辛格式在一定的条件下有着较好的误差精度.
  • 微分、差分方程的机械化方法
    高小山;李子明
    系统科学与数学. 2009, 29(9): 1222-1237. https://doi.org/10.12341/jssms08451
    摘要 ( ) PDF全文 ( )   可视化   收藏
    介绍了微分与差分方程机械化方法研究若干最新进展.主要结果包括: 微分、差分方程的特征列理论与算法,微分、差分方程系统的分解算法以及微分、差分方程解析解求解算法.
  • 基于指标形式张量的微分几何定理机器证明
    叶征;曹源昊;谢正;李洪波
    系统科学与数学. 2009, 29(9): 1238-1248. https://doi.org/10.12341/jssms08453
    摘要 ( ) PDF全文 ( )   可视化   收藏
    提出了一个基于指标形式张量的微分几何定理的机器证明算法.该算法将微分几何定理转化成带指标的张量多项式的计算问题,然后通过利用重写规则,挖掘等价条件和分次选取条件等方法大大减少了这个多项式系统的方程个数.再利用这个多项式系统本身和关于哑元的方程三角化这个多项式系统,将所得到的首项代入结论, 从而得到了该定理的机器证明.该算法不仅能够证明基于指标形式张量的微分几何定理,也可以用于张量方程的求解.
  • 多变量多项式矩阵素分解的结果和问题
    王明生
    系统科学与数学. 2009, 29(9): 1249-1255. https://doi.org/10.12341/jssms08456
    摘要 ( ) PDF全文 ( )   可视化   收藏
    多变量矩阵素分解问题是多维系统和信号处理学科中的基本问题,从提出以来,已经经过众多学者的研究.近年来随着符号代数计算的快速发展,情况有了根本的改变.概述近几年来该领域的研究进展情况和一些相关未解决的问题,从中可以看出该领域的研究密切依赖于机械化数学的研究进展.作为多变多项式矩阵分解理论的应用,给出两个变量多项式矩阵分解存在性定理的新证明.从中可以看出,2个变量多项式矩阵和3个以上变量矩阵的本质区别.
  • 三维Lotka-Volterra系统的动力学行为与极限环构造
    罗勇;陆征一
    系统科学与数学. 2009, 29(9): 1256-1265. https://doi.org/10.12341/jssms08455
    摘要 ( ) PDF全文 ( )   可视化   收藏
    综述三维Lotka-Volterra系统的动力学行为研究的新进展，主要是极限环的算法化构造与个数问题,以及一些相关猜想. 讨论了一些计算机辅助推理在种群动力学中的应用以及相关的问题.
  • 布尔环上的分支Grobner基算法
    孙瑶;王定康
    系统科学与数学. 2009, 29(9): 1266-1277. https://doi.org/10.12341/jssms08457
    摘要 ( ) PDF全文 ( )   可视化   收藏
    众所周知Gr\"obner基在很多领域都有着十分重要的应用.近些年来Gr\"obner基算法有了很大的改进,其中最著名的是Faug\`ere提出的F4和F5算法. 这两个算法具有很高的效率但通常需要消耗大量的内存.鉴于此,将给出一个布尔环上基于zdd数据结构的分支Gr\"obner基算法,该算法不仅可以大大降低对内存的消耗,还能有效的控制矩阵规模,从而提高算法的整体效率.详细阐述并证明了算法的基本理论,介绍该分支算法的数据结构及分支策略.最后通过实验数据可以发现,在很多例子中此算法都要优于Magma中的F4算法.
  • 变系数KdV-Burgers-Kuramoto方程的群论分析---容许变换及对称群
    闫振亚;谢福鼎
    系统科学与数学. 2009, 29(9): 1278-1285. https://doi.org/10.12341/jssms08458
    摘要 ( ) PDF全文 ( )   可视化   收藏
    提出变系数KdV-Burgers-Kuramoto(VCKdVBK)方程$u_t+f(x,t)uu_x+g(x,t)u_{xx}+h(x,t)u_{xxx}+k(x,t)u_{xxxx}=0$的容许变换, 它不改变方程的形式但可能改变方程的系数$f, g, h$及$k$.然后, 基于这个容许变换, 给出了VCKdVBK方程的7种不同类型的等价类. 最后, 也给出了VCKdVBK方程的Lie点对称群.
  • 四元数的复数形式及其在$6R$机器人反解中的应用
    廖启征;倪振松;李洪波;黄雷
    系统科学与数学. 2009, 29(9): 1286-1296. https://doi.org/10.12341/jssms08460
    摘要 ( ) PDF全文 ( )   可视化   收藏
    把四元数应用于平面旋转的特殊情况,并把旋转角度的正弦、余弦改写为复指数形式,导出平面四元数的两个复数形式的基.利用这两个基可以把表示三维变换的四元数和对偶四元数改造为复数形式,得到复数形式四元数的4个基和复数形式对偶四元数的8个基,以及它们之间乘法运算的运算法则.
    通过把它们应用到空间$6R$机器人的位移反解问题,证明了Dixon结式展开后的次数为16次,而不是形式上的24次,并且得到单变量的16次方程.
在线期刊
新闻公告 更多