• 论文 •

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

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

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

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.