On the Satisfiability of Linear Systems of Equations for Quantifiers  

作　　者：李廉 李慧陵 刘义循 

机构地区：[1]Department of Computer Science, Lanzhou University Lanzhou 730000 PRC [2]Department of Mathematics, Zhejiang University Hangzhou 310027 PRC [3]Department of Mathematics, Lanzhou University Lanzhou 730000 PRC

出　　处：《Science China Mathematics》1993年第4期385-393,共9页中国科学：数学（英文版）

基　　金：Project supported by the National Natural Science Foundation of China.

摘　　要：In this paper, the satisfiability problem of a linear system of equations for quantifiers is discussed. This problem arises from the mechanical theorem-proving on modules. A discriminating condition for this problem is obtained which places no restriction on quantifiers. Some applications to Abelian groups, elementary number theory, vector spaces, ect. are discussed.In this paper, the satisfiability problem of a linear system of equations for quantifiers is discussed. This problem arises from the mechanical theorem-proving on modules. A discriminating condition for this problem is obtained which places no restriction on quantifiers. Some applications to Abelian groups, elementary number theory, vector spaces, ect. are discussed.

关 键 词：module mechanical theorem-proving LINEAR system of EQUATIONS alge braic SYMBOLIC computation. 

分 类 号：N[自然科学总论]