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; 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/

由波兰数学学会与Biallystok技术大学和Biallystok大学合作主持的第六次数学会议（6pcm）将于2014年7月1日至4日在波兰的Biallystok举行。这项赠款将为来自美国的六名研究人员提供支持，参加由Artur Kornilowi​​cz组织的6pcm特别会议，并在Andrzej Trybulec的纪念馆中名为“数学的计算机辅助形式化”。 特别的会议纪念最早的形式化系统之一Mizar的创始人，将致力于计算机支持的数学形式化的各个方面。会议所涵盖的主题列表包括：具有挑战性的数学问题的形式化，互动性和自动化定理证明，证明助手的发展，证明语言和技术的设计，形式化数学的存储库，数学知识的语义表示，正式的知识，正式的工具，计划验证，基础和验证辅助工具的辅助工具，以及在教育中进行了验证。数学问题的形式化。该领域的研究得到了发展，用于开发用于数学的实际形式化系统（证明助手），建立了大量计算机验证的正式数学存储库以及定理证明的交互式和自动化方法的整合。证明助手提供了一种非常有用的教学工具，适合本科教学，特别是用于培训学生写严格证明的培训。会议网站位于http://katmat.pb.bialystok.pl/pcm14/