This paper discusses two problems:one is some important theories and algorithms of affine bracket algebra;the other is about their applications in mechanical theorem proving.First we give some efficient algorithms inc...This paper discusses two problems:one is some important theories and algorithms of affine bracket algebra;the other is about their applications in mechanical theorem proving.First we give some efficient algorithms including the boundary expanding algorithm which is a key feature in application.We analyze the characteristics of the boundary operator and this is the base for the implementation of the system.We also give some new theories or methods about the exact division,the representations and structure of affine geometry and so on.In practice,we implement the mechanical auto-proving system in Maple 10 based on the above algorithms and theories.Also we test about more than 100 examples and compare the results with the methods before.展开更多
This paper investigates complex brackets and balanced complex 1st-order difference (BCD) polynomials. Then we propose an algorithm of O(n log n) complexity to check the equality of brackets. It substitutes exponential...This paper investigates complex brackets and balanced complex 1st-order difference (BCD) polynomials. Then we propose an algorithm of O(n log n) complexity to check the equality of brackets. It substitutes exponential algorithms before. Also, BCD polynomials have some usages in geometric calculation.展开更多
基金This work was supported by the National Natural Science Foundation of China(Grant No.10471143)
文摘This paper discusses two problems:one is some important theories and algorithms of affine bracket algebra;the other is about their applications in mechanical theorem proving.First we give some efficient algorithms including the boundary expanding algorithm which is a key feature in application.We analyze the characteristics of the boundary operator and this is the base for the implementation of the system.We also give some new theories or methods about the exact division,the representations and structure of affine geometry and so on.In practice,we implement the mechanical auto-proving system in Maple 10 based on the above algorithms and theories.Also we test about more than 100 examples and compare the results with the methods before.
基金supported by the National Key Basic Research Project of China (Grant No. 2004CB318001)
文摘This paper investigates complex brackets and balanced complex 1st-order difference (BCD) polynomials. Then we propose an algorithm of O(n log n) complexity to check the equality of brackets. It substitutes exponential algorithms before. Also, BCD polynomials have some usages in geometric calculation.
