Limits of theory sequences over algebraically closed fields and applications Original Research Article

A computation model involving the computation of the limits of theory sequences is formally defined. It is called procedure scheme. It provides an approach to build a new theory by the limit of some sequence of formal theories and also has potential applications to scientific and engineering problems. A syntactic transformation system is described, which can transform any algebraically closed field (ALC) theory into a system of polynomial equations syntactically. The system provides a bridge to use the symbolic, algebraic computation techniques for studying the computational properties of procedure schemes. Some convergent procedure schemes are defined and investigated in the ALC. As applications of the framework, some procedure schemes in automated reasoning are designed, and a process of solving the center-focus problem for differential dynamical systems is described in such a way.