期刊文献+
共找到3篇文章
< 1 >
每页显示 20 50 100
数学机械化中的AC=BD模式 被引量:4
1
作者 张鸿庆 《系统科学与数学》 CSCD 北大核心 2008年第8期1030-1039,共10页
介绍了AC=BD模式及其在用机械化方法求解方程和证明定理中的应用.首先证明对可单值化算子D,如果CKerD(?)KerA,则存在算子B使AC=BD.利用带余除法对于给定的算子A给出了求其C-D对的算法,使得AC=BD.并将其应用到求解算子方程,可以将一些较... 介绍了AC=BD模式及其在用机械化方法求解方程和证明定理中的应用.首先证明对可单值化算子D,如果CKerD(?)KerA,则存在算子B使AC=BD.利用带余除法对于给定的算子A给出了求其C-D对的算法,使得AC=BD.并将其应用到求解算子方程,可以将一些较为复杂的方程化为简单方程求解.其次,利用对偶算子给出了将非线性非交换算子方程组化为单个方程求解的算法.最后,利用解方程的方法给出了机械化产生并证明定理的模式,并且给出了一些实例. 展开更多
关键词 AC=BD模式 解方程 数学机械化 证定理.
原文传递
Simplification and normalization of indexed differentials involving coordinate transformation 被引量:4
2
作者 LIU Jiang LI HongBo CAO YuanHao 《Science China Mathematics》 SCIE 2009年第10期2266-2286,共21页
In nD differential geometry, basic geometric structures and properties are described locally by differentiable functions and equations with indices that obey Einstein summation convention. Although symbolic manipulati... In nD differential geometry, basic geometric structures and properties are described locally by differentiable functions and equations with indices that obey Einstein summation convention. Although symbolic manipulation of such indexed functions is one of the oldest research topics in computer algebra, so far there exists no normal form reduction algorithm to judge whether two indexed polynomials involving indices of different coordinate systems are equal or not. It is a challenging task in computer algebra. In this paper, for a typical framework—the partial derivatives in coordinate transformation matrix involved are of order no more than two (such as local computations of ordinary curvatures and tor-sion), we put forward two algorithms, one on elimination of all redundant dummy indices of indexed polynomials, the other on normalization of such indexed polynomials, by which we can judge whether two indexed polynomials are equal or not. We implement the algorithms with Maple V.10 and use them to solve tensor verification problems in differential geometry, and to derive automatically the transformation rules of locally defined indexed functions under the change of local coordinates. 展开更多
关键词 nD symbolic computation Einstein summation convention mechanical theorem-proving differential geometry tensor verification 68W30 53-99
原文传递
带量词的合一算法
3
作者 李大法 《清华大学学报(自然科学版)》 EI CAS CSCD 北大核心 1992年第3期30-36,共7页
Robinson于 1965年提出了归结原理,其主要工作是 Unification算法。这个算法只能处理不带量词的子句公式,它不能用来发现定理的自然演绎证明。本文的算法能处理量词,它能用在基于自然演绎的定理证明系统上。... Robinson于 1965年提出了归结原理,其主要工作是 Unification算法。这个算法只能处理不带量词的子句公式,它不能用来发现定理的自然演绎证明。本文的算法能处理量词,它能用在基于自然演绎的定理证明系统上。文中给出合一定理的证明,基于此算法的自动自然演绎系统已实现,用它证明了Andrews;Bledsoe和Pellotier挑战性问题。 展开更多
关键词 自然演绎 一阶逻辑 归结 合一算法
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部