基于数学归纳法抽取循环程序研究

广义上，程序设计过程就是定理证明过程，因而程序综合与机器定理证明关系密切。由于归结原理的反证法本质，不能保证其证明是构造性的，因此不能保证能够抽取循环程序，但是利用数学归纳法可以使用归结原理来抽取循环体，从而抽取循环程序。文中利用数学归纳法进行了循环程序的提取。

The Study on Extraction Loop program Based on Mathematical Induction

In general, design of program can be treated as theorem proving, so program synthesis has close relations with automatic theorem proving. Essentially, not all of the proving of resolution principle is constructive so not all loop program canbe extracted form the proving. But loop program can be extracted from the proving of resolution principle with the aid ofmathematical induction. In this paper, the aid of mathematical induction is used to extract..