The Model AC=BD for Mathematics Mechanization
数学机械化中的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.