Proof Animation -testing proofs by constructive programming-

证明动画 - 通过构造性编程测试证明 -

• 批准号: 10480063
• 负责人: HAYASHI Susumu
• 金额: $ 4.03万
• 依托单位: Kobe University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B).
• 财政年份: 1998
• 资助国家: 日本
• 起止时间: 1998 至 2000
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-10480063/
• 关键词: constructive programming; program verification; program logic; learning theory; classical proof execution; 学習理論

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.

对经典证明执行的一些理论进行了检验，看它们是否适用于证明动画。我们用Ogata理论为PA实现了一个环境，并在简单的测试中进行了测试。贝拉尔迪理论也通过计算机实验从理论和实践上得到了深入的检验。为了突破现有理论的局限性，我们提出了一种新的经典证据执行理论。它是基于算法学习理论的思想，与现有的理论完全不同。该理论称为极限可计算数学(LCM)。研究了LCM在PA中的应用。也许，更重要的是，事实证明，LCM与计算机科学和逻辑中的各种理论有着许多深刻的联系。例如实数计算、递归理论中的基本定理、经典逻辑原理的逆数学、并行计算、不变理论的计算机代数等。这一想法激励了许多研究人员，一些独立于我们或与我们合作的项目正在进行。

项目成果

M.Banbara and N.Tamura: "Compiling Resources in a Linear Logic Programming Language"Proc.of Workshop on Parallelism and Implementation Techonology for Logic Programming Languages. 32-45 (1998)

M.Banbara 和 N.Tamura：“用线性逻辑编程语言编译资源”Proc.of Workshop on Parallelism and Implementing Techonology for LogicProgramming Languages。

M.Yasugi: "Effective properties of sets and functions in metric spaces with computability structure"Theoretical Computer Science. 219. 467-486 (1999)

M.Yasugi：“具有可计算结构的度量空间中集合和函数的有效性质”理论计算机科学。

S. Hayashi: "Formalized Mathematics, Proof Animation, and Limit Computable Mathematics"Relevance and Feasibility of Mathematical Analysis on the Computer, RIMS, Kyoto, March 21/22, 数理解析研究所講究録. (2000)

S. Hayashi：“形式化数学、证明动画和极限可计算数学”计算机数学分析的相关性和可行性，RIMS，京都，3 月 21 日/22 日，数学分析研究所 Kokyuroku（2000 年）。

S. Hayashi: "Towards Animation of Proofs"Theoretical Computer Science. (未定). (2001)

S. Hayashi：“走向证明动画”理论计算机科学（待定）。

R.Sumitomo, S.Hayashi: "A proof animation environment"Computer Software(in Japanese). Vol.16, No.3. 71-74 (1999)

R.Sumitomo、S.Hayashi：“证明动画环境”计算机软件（日语）。