• 论文 • 上一篇    下一篇

数学机械化中的AC=BD模式

张鸿庆   

  1. 大连理工大学应用数学系, 大连 116024
  • 收稿日期:2007-12-29 修回日期:1900-01-01 出版日期:2008-08-25 发布日期:2008-08-25

张鸿庆. 数学机械化中的AC=BD模式[J]. 系统科学与数学, 2008, 28(8): 1030-1039.

ZHANG Hongqing. The Model AC=BD for Mathematics Mechanization[J]. Journal of Systems Science and Mathematical Sciences, 2008, 28(8): 1030-1039.

The Model AC=BD for Mathematics Mechanization

ZHANG Hongqing   

  1. Department of Applied Mathematics, Dalian University of Technology, Dalian 116024
  • Received:2007-12-29 Revised:1900-01-01 Online:2008-08-25 Published:2008-08-25
介绍了AC=BD模式及其在用机械化方法求解方程和证明定理中的应用.首先证明对可单值化算子D, 如果C Ker D \subset Ker A, 则存在算子B使AC=BD.利用带余除法对于给定的算子A给出了求其C-D对的算法,使得AC=BD. 并将其应用到求解算子方程, 可以将一些较为复杂的方程化为简单方程求解.其次, 利用对偶算子给出了将非线性非交换算子方程组化为单个方程求解的算法.最后, 利用解方程的方法给出了机械化产生并证明定理的模式, 并且给出了一些实例.
The model AC=BD is presented, which can be applied to mechanical equations-solving and theorem-proving.First, it is proved that for an uniformizable operator D, there exists an operator B such that AC=BD if C Ker D \subset Ker A.By using division with remainder, an approach to compute the C-D pair is given for a given operator A such that AC=BD, which can be applied to solve operator equations.
Hence some complex equations can be reduced to the simple ones.Then in terms of dual operators, an approach to reduce nonlinear and noncommutative operator systems to a single equation is given.Finally, by use of the methods of solving equations,we present a model need to produce and prove theorems mechanically is presented, and some examples are listed.

MR(2010)主题分类: 

()
[1] 鲁健, 曾振柄. 用符号计算证明Ramsey定理的一个机械化方法[J]. 系统科学与数学, 2021, 41(12): 3311-3323.
[2] 宋丽平,余王辉. 经理期权整体实施与非限制实施的等价[J]. 系统科学与数学, 2016, 36(10): 1710-1720.
[3] 曾振柄;张景中. 基于矩形区域剖分的不等式机器证明方法---以Zirakzadeh的一个几何不等式为例[J]. 系统科学与数学, 2010, 30(11): 1430-1458.
[4] 高小山;李子明. 微分、差分方程的机械化方法[J]. 系统科学与数学, 2009, 29(9): 1222-1237.
[5] 石赫. Yang-Mills规范场的存在性、可解性(一)[J]. 系统科学与数学, 2009, 29(9): 1200-1210.
[6] 吴文俊. 数学机械化研究回顾与展望[J]. 系统科学与数学, 2008, 28(8): 898-904.
[7] 石赫. SU(2)规范场的恰当形式(欧空间)[J]. 系统科学与数学, 2008, 28(7): 859-866.
[8] 李树荣. SISO多维控制系统的反馈镇定性及算法的数学机械化实现[J]. 系统科学与数学, 2001, 21(2): 147-151.
阅读次数
全文


摘要