11月27日,刘志明教授在ChinaSoft 2022形式化方法教育论坛分享数理逻辑是计算机科学与系统的天然基础报告。
本次ChinaSoft 2022是由中国计算机学会(CCF)主办,CCF软件工程专委会、系统软件专委会、形式化方法专委会、复旦大学承办。本次大会的主题为“聚焦产教研用协同创新,提升关键软件供给能力”。
刘志明教授在报告中通过对逻辑的内涵与外延、逻辑的形式化、形式的逻辑系统、程序逻辑的介绍,让与会者深刻意识到:在计算机科学与工程技术快速发展的时代下,更需要回过头审视它的核心基础,以及思考从图灵机到人机物融合系统的演进发展。
刘志明教授指出,计算机只能处理符号语言而不理解“内容”,并且程序语言和逻辑语言的定义的思想和方法一致,程序的执行等同于逻辑证明。为此,提出要严谨理解泛在计算、IoT、软件定义一切、AI、人机物融合系统,即它们不能停留在图示、抽象的概念或愿景;而必须成为符号化的程序,按照逻辑规则处理符号表示的数据。
在报告的最后刘志明教授提出形式化方法的重要性不仅在工程技术方面和工具方面,更在基础的认知方面;好的数理逻辑支持掌握和研究新的计算模型和系统。为此,刘志明教授提议要加强本科生数理逻辑教育和实践、培养学生知识的基础性和关联性、思想和方法的系统性、和深度思考的习惯。
本次报告中,刘志明教授的报告传达的重要思想包括以下几点:
1.逻辑研究建立概念、个体、关系、命题和推理判断的关系,对认知是重要的。
2.形式逻辑的核心思想是命题和推理的形式与内容的分离,推理的有效性由推理的形式决定。
3.一个形式逻辑系统是一个形式语言,推理证明系统,语言语义基础上的推理系统的模型的三位一体。
4.计算模型,图灵机、递归函数论和lambda演算都是形式系统。
5.程序语言,其语义和程序证明构成一个形式系统。
(通讯报导:李玉祥;审校:刘波)