论文部分内容阅读
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