%0 Journal Article
%T The Model AC=BD for Mathematics Mechanization<br>数学机械化中的AC=BD模式
%A ZHANG Hongqing
%A <br>张鸿庆
%J 系统科学与数学
%D 2008
%I 
%X 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.
%K Model AC=BD
%K equation solving
%K mathematics mechanization
%K theorem proving<br>AC=BD模式
%K 解方程
%K 数学机械化
%K 证定理
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=6E709DC38FA1D09A4B578DD0906875B5B44D4D294832BB8E&cid=37F46C35E03B4B86&jid=0CD45CC5E994895A7F41A783D4235EC2&aid=B4DB7D7E5CC8FAB2318EAE8274806597&yid=67289AFF6305E306&vid=D3E34374A0D77D7F&iid=5D311CA918CA9A03&sid=0342E221E01D5238&eid=C7A7E1E32985D389&journal_id=1000-0577&journal_name=系统科学与数学&referenced_num=1&reference_num=12