Toward a practical, mechanically checkable reasoning environment

走向实用的、可机械检查的推理环境

• 批准号: 9207-2008
• 负责人: Rudnicki, Piotr
• 金额: $ 1.17万
• 依托单位: University of Alberta
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2010
• 资助国家: 加拿大
• 起止时间: 2010-01-01 至 2011-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=450441
• 关键词: Toward; practical; mechanically; checkable; reasoning

Rigorous mathematical techniques find more and more applications in specification and development of complex systems. Automating the process of checking that the mathematics has been properly used is desirable not only in applications but in conducting mathematical research. This leads to the grand idea of building a computerized verification system that represents all important mathematical knowledge and techniques. For more than three decades, I have been involved in a project named Mizar that has attempted to build a modest, trial version of such a system.

严格的数学技术在复杂系统的规范和开发中得到越来越多的应用。 自动化的过程检查数学已经被正确地使用是可取的，不仅在应用程序中，但在进行数学研究。 这导致了建立一个计算机化的验证系统，代表所有重要的数学知识和技术的宏伟构想。 三十多年来，我一直参与一个名为Mizar的项目，试图建立一个这样一个系统的适度，试用版。