Formalizing a Reasoning Strategy in Symbolic Approach to Differential Equations
Shilong Ma · Birkhäuser-Verlag eBooks · 2006
There is a reasoning strategy, which is an incremental computation, used in symbolic and algebraic approach to differential equations. The center-focus problem can be solved by using this reasoning strategy. In algebraic approach to automated reasoning, the construction of polynomial ideals is at the heart. For polynomials with a known fixed number of variables, the problem of constructing polynomial ideals can be solved by the Gröbner basis method and Wu’s method. However, in many cases, the concerned polynomials may contain arbitrarily many variables. Even for the case of polynomials with a fixed number of variables, sometimes we do not know the number in advance, and we only know that there exists such a number. Thus, it is necessary to theoretically study how to construct ideals for polynomial sets with arbitrarily many variables. In this paper, a model for incremental computations, called procedure scheme, is proposed, and based on this model the well limit behavior of incremental computations is studied. It provides an approach to build a new theory by the limit of a sequence of formal theories. A convergent procedure scheme, DISCOVER, is defined in algebraically closed fields. We can formalize the strategy mentioned above using the procedure scheme DISCOVER.