Computer-assisted Formalization of Mathematics, 6th Podlasie Conference, Bialystok, July 1-4, 2014

计算机辅助数学形式化，第六届 Podlasie 会议，比亚韦斯托克，2014 年 7 月 1-4 日

• 批准号: 1419326
• 负责人: Krystyna Kuperberg
• 金额: $ 1万
• 依托单位: Auburn University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-03-15 至 2016-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1419326&HistoricalAwards=false
• 关键词: Computer; assisted; Formalization; Mathematics; 6th

The 6th Podlasie Conference on Mathematics (6PCM), hosted by the Polish Mathematical Society in cooperation with the Bialystok University of Technology and the University of Bialystok, will be held July 1-4, 2014, in Bialystok, Poland. This grant will provide support for six researchers from the United States to participate in the 6PCM Special Session organized by Artur Kornilowicz and entitled Computer-assisted Formalization of Mathematics --- In memoriam of Andrzej Trybulec. The special session, honoring the founder of Mizar, one of the earliest formalization systems, will be devoted to all aspects of computer-supported formalization of mathematics. The list of topics covered by the session includes: formalization of challenging mathematical problems, interactive and automated theorem proving, development of proof assistants, design of proof languages and techniques, repositories of formalized mathematics, semantic representation of mathematical knowledge, formal tools in program verification, foundations and philosophy of mathematics, and proof assistants in education.Over the last decades, we witnessed a number of successful instances of computer-assisted formalization of mathematical problems. Research in this field has been boosted by the development of systems for practical formalization of mathematics (proof assistants), a creation of large repositories of computer-verified formal mathematics, and integration of interactive and automated methods of theorem proving. Proof assistants provide a very useful teaching tool suitable for undergraduate instruction, in particular for training beginning students in writing rigorous proofs. The meeting website is at http://katmat.pb.bialystok.pl/pcm14/

由波兰数学会与比亚韦斯托克理工大学和比亚韦斯托克大学合作主办的第六届波德拉西数学会议（6PCM）将于2014年7月1日至4日在波兰比亚韦斯托克举行。这笔赠款将支持来自美国的六名研究人员参加 Artur Kornilowi​​cz 组织的 6PCM 特别会议，题为“计算机辅助数学形式化——纪念 Andrzej Trybulec”。 这次特别会议旨在纪念最早的形式化系统之一 Mizar 的创始人，将致力于计算机支持的数学形式化的各个方面。会议涵盖的主题列表包括：具有挑战性的数学问题的形式化、交互式和自动化定理证明、证明助手的开发、证明语言和技术的设计、形式化数学的存储库、数学知识的语义表示、程序验证中的形式化工具、数学基础和哲学，以及教育证明助理。在过去的几十年里，我们目睹了许多计算机辅助数学问题形式化的成功实例。数学实用形式化系统（证明助手）的开发、计算机验证形式数学大型存储库的创建以及交互式和自动化定理证明方法的集成，推动了该领域的研究。证明助手提供了一个非常有用的教学工具，适合本科教学，特别是训练初学者编写严格的证明。会议网站：http://katmat.pb.bialystok.pl/pcm14/