Two inference rules are discussed in boolean ring based theorem proving, and linear strategy is developed. It is shown that both of them are complete for linear strategy. Moreover, by introducing a partial ordering on...Two inference rules are discussed in boolean ring based theorem proving, and linear strategy is developed. It is shown that both of them are complete for linear strategy. Moreover, by introducing a partial ordering on atoms, pseudo O-linear and O-linear strategies are presented. The former is complete, the latter,however, is complete for clausal theorem proving.展开更多
In this paper,the I-ring which satisfies almost descending chain conditions (shorten writting A. D. C. C) on principal left ideals is studied. Two main results are gaven: (1) I-ring which satisfies A. D.C. C on princi...In this paper,the I-ring which satisfies almost descending chain conditions (shorten writting A. D. C. C) on principal left ideals is studied. Two main results are gaven: (1) I-ring which satisfies A. D.C. C on principal left ideals is Boolen. (2) Ring with identity whose principal left ideals satisfy A. D. C. C and of which each element except identity is a left zero-divisor, is Boolean.These results generalize the results of [1],[2] and [3].展开更多
Some techniques using linear algebra was introduced by Faugore in F4 to speed up the reduction process during Grobner basis computations. These techniques can also be used in fast implementations of F5 and some other ...Some techniques using linear algebra was introduced by Faugore in F4 to speed up the reduction process during Grobner basis computations. These techniques can also be used in fast implementations of F5 and some other signature-based Grobner basis algorithms. When these techniques are applied, a very important step is constructing matrices from critical pairs and existing polynomials by the Symbolic Preprocessing function （given in F4）. Since multiplications of monomials and polynomials are involved in the Symbolic Preprocessing function, this step can be very costly when the number of involved polynomials/monomials is huge. In this paper, multiplications of monomials and polynomials for a Boolean polynomial ring are investigated and a specific method of implementing the Symbolic Preprocessing function over Boolean polynomial rings is reported. Many examples have been tested by using this method, and the experimental data shows that the new method is very efficient.展开更多
文摘Two inference rules are discussed in boolean ring based theorem proving, and linear strategy is developed. It is shown that both of them are complete for linear strategy. Moreover, by introducing a partial ordering on atoms, pseudo O-linear and O-linear strategies are presented. The former is complete, the latter,however, is complete for clausal theorem proving.
文摘In this paper,the I-ring which satisfies almost descending chain conditions (shorten writting A. D. C. C) on principal left ideals is studied. Two main results are gaven: (1) I-ring which satisfies A. D.C. C on principal left ideals is Boolen. (2) Ring with identity whose principal left ideals satisfy A. D. C. C and of which each element except identity is a left zero-divisor, is Boolean.These results generalize the results of [1],[2] and [3].
基金supported by the National Key Basic Research Program of China under Grant Nos.2013CB834203 and 2011CB302400the National Nature Science Foundation of China under Grant Nos.11301523,11371356,61121062+1 种基金the Strategic Priority Research Program of the Chinese Academy of Sciences under Grant No.XDA06010701IEE’s Research Project on Cryptography under Grant Nos.Y3Z0013102,Y3Z0018102,and Y4Z0061A02
文摘Some techniques using linear algebra was introduced by Faugore in F4 to speed up the reduction process during Grobner basis computations. These techniques can also be used in fast implementations of F5 and some other signature-based Grobner basis algorithms. When these techniques are applied, a very important step is constructing matrices from critical pairs and existing polynomials by the Symbolic Preprocessing function （given in F4）. Since multiplications of monomials and polynomials are involved in the Symbolic Preprocessing function, this step can be very costly when the number of involved polynomials/monomials is huge. In this paper, multiplications of monomials and polynomials for a Boolean polynomial ring are investigated and a specific method of implementing the Symbolic Preprocessing function over Boolean polynomial rings is reported. Many examples have been tested by using this method, and the experimental data shows that the new method is very efficient.
