The scientific proof is the highest type of the rational proof. The mankind is looking for the best technology of the reasonable demonstration. What is a proof？. What is a scientific proof？. Philosophical investigat...The scientific proof is the highest type of the rational proof. The mankind is looking for the best technology of the reasonable demonstration. What is a proof？. What is a scientific proof？. Philosophical investigations of proofs have the long history. Philosophy is exploring physics, mathematics, astronomy, biology, history, and so on. Science demands strict proofs. Science uses the specific methods as the optimum technologies for the achievement of the truth. Strictness of the proof depends on the aim algorithm： the distribution of the functions between parts of the proof. The beginning stage, the middle parts, and the ending stage are the unit of the proof. Philosophy can make the correct model of the scientific proof only! Science and its methodology develop and the growth of knowledge has not the finish. The rational ideals improve continually. Science is looking for the criterion of the demonstrative strictness. The adaptation algorithm of the scientific method is the best technology for the achievement of the truth.展开更多
The authors consider relational databases organized over an ordered domain with some additional relations - a typical example is the ordered domain of rational numbers together with the operation of addition. In the f...The authors consider relational databases organized over an ordered domain with some additional relations - a typical example is the ordered domain of rational numbers together with the operation of addition. In the focus of our study are the FO （first-order） queries that are invariant under order-preserving permutations-such queries are called order-generic. It was discovered that for some domains order-generic FO queries fail to express more than pure order queries. The collapse result theorem was proved for locally genetic queries over a linearly ordered domain with the Pseudo finite Homogeneity Property （or / and the Isolation Property） by Belegradek et al.. Here the authors consider a circularly ordered domain and prove the collapse result theorem over a quasi circularly minimal domain.展开更多
In 2002, Faugere presented the famous F5 algorithm for computing GrSbner basis where two cri- teria, syzygy criterion and rewritten criterion, were proposed to avoid redundant computations. He proved the correctness o...In 2002, Faugere presented the famous F5 algorithm for computing GrSbner basis where two cri- teria, syzygy criterion and rewritten criterion, were proposed to avoid redundant computations. He proved the correctness of the syzygy criterion, but the proof for the correctness of the rewritten criterion was left. Since then, F5 has been studied extensively. Some proofs for the correctness of F5 were proposed, but these proofs are valid only under some extra assumptions. In this paper, we give a proof for the correctness of F5B, an equivalent version of F5 in Buchberger＇s style. The proof is valid for both homogeneous and non-homogeneous polynomial systems. Since this proof does not depend on the computing order of the S-pairs, any strategy of selecting S-pairs could be used in F5B or F5. Furthermore, we propose a natural and non-incremental variant of F5 where two revised criteria can be used to remove almost all redundant S-pairs.展开更多
The problem of navigation for the distributed satellites system using relative range mea- surements is investigated. Firstly, observability for every participating satellites is analyzed based on the nonlinear Kepleri...The problem of navigation for the distributed satellites system using relative range mea- surements is investigated. Firstly, observability for every participating satellites is analyzed based on the nonlinear Keplerian model containing J2 perturbation and the nonlinear measurements. It is proven that the minimum number of tracking satellites to assure the observability of the distributed satellites system is three. Additionally, the analysis shows that the J2 perturbation and the nonlinearity make little contribution to improve the observability for the navigation. Then, a quasi-consistent extended Kalman filter based navigation algorithm is proposed, which is quasi-consistent and can provide an on- line evaluation of the navigation precision. The simulation illustrates the feasibility and effectiveness of the proposed navigation algorithm for the distributed satellites system.展开更多
In this paper, the following are introduced briefly： the basic concept of q-proper-hypergeometric; an algorithmic proof theory for q-proper-hypergeometric identities; and elimination in the non- commutative Weyl alge...In this paper, the following are introduced briefly： the basic concept of q-proper-hypergeometric; an algorithmic proof theory for q-proper-hypergeometric identities; and elimination in the non- commutative Weyl algebra. We give an algorithm for proving the single-variable q-proper-hypergeometric identities that is based on Zeilberger＇s approach and the elimination in Weyl algebra. Finally, we test several examples that have been proven by D. Zeilberger and H. Will using the WZ-pair method and Gosper algorithm.展开更多
文摘The scientific proof is the highest type of the rational proof. The mankind is looking for the best technology of the reasonable demonstration. What is a proof？. What is a scientific proof？. Philosophical investigations of proofs have the long history. Philosophy is exploring physics, mathematics, astronomy, biology, history, and so on. Science demands strict proofs. Science uses the specific methods as the optimum technologies for the achievement of the truth. Strictness of the proof depends on the aim algorithm： the distribution of the functions between parts of the proof. The beginning stage, the middle parts, and the ending stage are the unit of the proof. Philosophy can make the correct model of the scientific proof only! Science and its methodology develop and the growth of knowledge has not the finish. The rational ideals improve continually. Science is looking for the criterion of the demonstrative strictness. The adaptation algorithm of the scientific method is the best technology for the achievement of the truth.
文摘The authors consider relational databases organized over an ordered domain with some additional relations - a typical example is the ordered domain of rational numbers together with the operation of addition. In the focus of our study are the FO （first-order） queries that are invariant under order-preserving permutations-such queries are called order-generic. It was discovered that for some domains order-generic FO queries fail to express more than pure order queries. The collapse result theorem was proved for locally genetic queries over a linearly ordered domain with the Pseudo finite Homogeneity Property （or / and the Isolation Property） by Belegradek et al.. Here the authors consider a circularly ordered domain and prove the collapse result theorem over a quasi circularly minimal domain.
基金supported by National Key Basic Research Project of China (Grant No.2011CB302400)National Natural Science Foundation of China (Grant Nos. 10971217 and 61121062)
文摘In 2002, Faugere presented the famous F5 algorithm for computing GrSbner basis where two cri- teria, syzygy criterion and rewritten criterion, were proposed to avoid redundant computations. He proved the correctness of the syzygy criterion, but the proof for the correctness of the rewritten criterion was left. Since then, F5 has been studied extensively. Some proofs for the correctness of F5 were proposed, but these proofs are valid only under some extra assumptions. In this paper, we give a proof for the correctness of F5B, an equivalent version of F5 in Buchberger＇s style. The proof is valid for both homogeneous and non-homogeneous polynomial systems. Since this proof does not depend on the computing order of the S-pairs, any strategy of selecting S-pairs could be used in F5B or F5. Furthermore, we propose a natural and non-incremental variant of F5 where two revised criteria can be used to remove almost all redundant S-pairs.
基金supported by the National Basic Research Program of China under Grant No.2014CB845303the National Center for Mathematics and Interdisciplinary Sciences,Chinese Academy of Sciences
文摘The problem of navigation for the distributed satellites system using relative range mea- surements is investigated. Firstly, observability for every participating satellites is analyzed based on the nonlinear Keplerian model containing J2 perturbation and the nonlinear measurements. It is proven that the minimum number of tracking satellites to assure the observability of the distributed satellites system is three. Additionally, the analysis shows that the J2 perturbation and the nonlinearity make little contribution to improve the observability for the navigation. Then, a quasi-consistent extended Kalman filter based navigation algorithm is proposed, which is quasi-consistent and can provide an on- line evaluation of the navigation precision. The simulation illustrates the feasibility and effectiveness of the proposed navigation algorithm for the distributed satellites system.
文摘In this paper, the following are introduced briefly： the basic concept of q-proper-hypergeometric; an algorithmic proof theory for q-proper-hypergeometric identities; and elimination in the non- commutative Weyl algebra. We give an algorithm for proving the single-variable q-proper-hypergeometric identities that is based on Zeilberger＇s approach and the elimination in Weyl algebra. Finally, we test several examples that have been proven by D. Zeilberger and H. Will using the WZ-pair method and Gosper algorithm.
