Proof Animation -testing proofs by constructive programming-

点击翻译按钮获取中文摘要

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.