Proof Animation -testing proofs by constructive programming-

对一些经典的打样执行理论进行了检验，看它们是否适用于打样动画。我们利用Ogata理论实现了一个PA环境，并在简单的例子上进行了测试。通过计算机实验，从理论和实践两个方面对贝拉尔迪理论进行了深入的检验。为了突破现有理论的局限性，我们发展了一种新的古典证据执行理论。它基于算法学习理论的思想，与现有的理论完全不同。研究了极限可计算数学在PA中的应用。也许，更重要的是，LCM与计算机科学和逻辑中的各种理论有着很深的联系。例子是计算的真实的数字，基础定理在递归理论，逆向数学的原则，古典逻辑，并发计算，计算机代数的不变理论，等等。这个想法刺激了许多研究人员，一些独立于我们或与我们合作的项目正在进行。

Some theories of classical proof exectution were examined if they are good for proof animation. We implemented an environment for PA by Ogata-theory and it was tested on simple examles. Berardi theory was also deeply examined theoretically and practically by a computer experiment. It turned out that existing theory are short for the aim.To break through the limitation of the existing theories, we developed a new theory of classical proof execution. It is based on the ideas from algorithmic learning theory and is entirely different from the existing theories. The theory is called LCM(Limit Computable Mathematics).Application of LCM to PA was investigated. Maybe, even more importantly, it turned out that LCM has a lot of deep connections to various theories in computer science and logic. Examples are computation on real numbers, basis theorems in recursion theory, reverse mathematics of principles of classical logic, concurrent computation, computer algebra of invariant theory, etc. etc.. This idea stimulated many researchers and some projects independent from and/or collaborated with us are taking place.