Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F. and Nipkow, T., Term Rewriting and All That. Cambridge University Press, Cambridge, 1998.
Buchberger, B., Gröbner bases: An algorithmic method in polynomial ideal theory. In: Recent Trends in Multidimensional Systems Theory (Bose, N. K., ed.), pp. 184–232. D. Reidel, Dordrecht, Holland, 1985.
James, E. M. and Lloyd, N. G., A cubic system with eight small-amplitude limit cycles. IMA J. Appl. Math. 47: 163–171, 1991.
Li, W., An open logic system (in Chinese). Science in China (Sci. Sinica) (ser. A) 10: 1103–1113, 1992.
Li, W. and Ma, S., A framework for analytic-intelligent agents. In: Proceedings of the International Conference on Artificial Intelligence (IC-AI’2000), Las Vegas, USA, 2000.
Li, W. and Ma, S., Limits of theory sequences over algebraically closed fields and applications. Discrete Appl. Math. 136(1): 23–43, 2004.
Ma, S., Sui, Y. and Xu, K., The limits of the Horn logic programs. In: Proceedings of the 18th International Conference on Logic Programming (ICLP 2002), Copenhagen, Denmark, LNCS 2401, p. 467. Springer-Verlag, Berlin Heidelberg, 2002.
Lu, Z. and Ma, S., Centers, foci and limit cycles for polynomial differential systems. In: Mathematics Mechanization and Applications (Gao, X.-S. and Wang, D., eds.), pp. 365–387. Academic Press, London, 2000.
Ma, S. and Ning, S., Deriving some new conditions on the existence of eight limit cycles for a cubic system. Comput. Math. Appl. 33: 59–84 1997.
Ma, S. and Ning, S., Practically solving some problems expressed in the first order theory of real closed fields. Int. J. Comput. Math. 69: 265–282, 1998.
Ma, S., A computational study on limit behavior of formal system sequences and its applications (in Chinese). Technical Report, School of Computer Science, Beihang University, December 2003.
Ning, S., Ma, S., Kwek, K. H. and Zheng, Z., A cubic system with eight small-amplitude limit cycles. Appl. Math. Lett. 7: 23–27, 1994.
Rabin, M., Decidable theories. In: Handbook of Mathematical Logic (Barwise, ed.), pp. 595–630. North-Holland Publ. Co., 1977.
Wang, D., Mechanical manipulation for a class of differential systems. J. Symb. Comput. 12: 233–254, 1991.
Wang, D., A method for proving theorems in differential geometry and mechanics. J. Univ. Comput. Sci. 1: 658–673, 1995.
Wu, W., On the mechanization of theorem-proving in elementary differential geometry (in Chinese). Sci. Sinica Special Issue on Math. (I): 94–102, 1979.
Wu, W., Basic principles of mechanical theorem proving in elementary geometries. J. Automat. Reason. 2: 221–252, 1986.
Wu, W., Mechanical theorem proving in elementary geometry and elementary differential geometry. In: Proceedings of the 1980 Beijing DD-Symposium, vol. 2, pp. 1073–1092. Science Press, Beijing, 1982.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Birkhäuser Verlag Basel/Switzerland
About this paper
Cite this paper
Ma, S. (2005). Formalizing a Reasoning Strategy in Symbolic Approach to Differential Equations. In: Wang, D., Zheng, Z. (eds) Differential Equations with Symbolic Computation. Trends in Mathematics. Birkhäuser Basel. https://doi.org/10.1007/3-7643-7429-2_10
Download citation
DOI: https://doi.org/10.1007/3-7643-7429-2_10
Publisher Name: Birkhäuser Basel
Print ISBN: 978-3-7643-7368-9
Online ISBN: 978-3-7643-7429-7
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)