博文
形式化方法实务简述
|||
一、形式化方法（formal methods）的定义：
形式化方法是用[人工符号（形式语言）和演绎体系]（形式系统）使理论严格化、精确化的程序和方法。具体方法是理论中的概念转化为符号、命题转化为符号公式、推演就是符号公式的推理变化。著名哲学家与逻辑史家波亨斯基（I.M.I.M.Bochenski,1902-1995)在<<当代思维方法>>中指出:"形式化系统总是按如下顺序形成的：先确定有意义的符号，然后从符号中抽象掉意义，并用形式化方法构成系统，最后对这个所构成的系统作一种新的诠释。“在计算机科学中有广泛的应用，比如程序设计语言设计、软件工程、程序验证、人工智能、语义网络、知识处理等，计算机科学相关专业要重视这方面的教学与研究，提升基础科学实力，系统软件科研与技术实力不如有的国家，是否有这方面的原因，我认为有，这是相关创新与发明的根基，现代逻辑课程对于计算机科学是相当有用的，有一些老一代科学家在这方面做了好多创新工作，应很好继承与发展，中科院软件所这方面有好的传递精神。
二、形式化方法的步骤：
（由具体到抽象）
步骤1、预备性研究（确定形式系统的成分及逻辑关系）
步骤2、构造形式系统：要解决两件事，一是形式语言构成问题、二是演绎体系形成问题，形式语言由符号表与语法规则构成，演绎体系是指以一阶逻辑为基础，进行变形的规则系统。
（由抽象到具体）
步骤3、最后形式系统(元逻辑）验证、应用、改进、扩展研究
三、学习方法：研究一些著名的形式系统及其应用，体会一下处理研究的思维方法.
https://blog.sciencenet.cn/blog-89075-238819.html
上一篇： Consequence-Driven Reasoning for Horn SHIQ Ontologies
下一篇：Structure and Interpretation of Computer Programs
形式化方法是用[人工符号（形式语言）和演绎体系]（形式系统）使理论严格化、精确化的程序和方法。具体方法是理论中的概念转化为符号、命题转化为符号公式、推演就是符号公式的推理变化。著名哲学家与逻辑史家波亨斯基（I.M.I.M.Bochenski,1902-1995)在<<当代思维方法>>中指出:"形式化系统总是按如下顺序形成的：先确定有意义的符号，然后从符号中抽象掉意义，并用形式化方法构成系统，最后对这个所构成的系统作一种新的诠释。“在计算机科学中有广泛的应用，比如程序设计语言设计、软件工程、程序验证、人工智能、语义网络、知识处理等，计算机科学相关专业要重视这方面的教学与研究，提升基础科学实力，系统软件科研与技术实力不如有的国家，是否有这方面的原因，我认为有，这是相关创新与发明的根基，现代逻辑课程对于计算机科学是相当有用的，有一些老一代科学家在这方面做了好多创新工作，应很好继承与发展，中科院软件所这方面有好的传递精神。
二、形式化方法的步骤：
（由具体到抽象）
步骤1、预备性研究（确定形式系统的成分及逻辑关系）
步骤2、构造形式系统：要解决两件事，一是形式语言构成问题、二是演绎体系形成问题，形式语言由符号表与语法规则构成，演绎体系是指以一阶逻辑为基础，进行变形的规则系统。
（由抽象到具体）
步骤3、最后形式系统(元逻辑）验证、应用、改进、扩展研究
三、学习方法：研究一些著名的形式系统及其应用，体会一下处理研究的思维方法.
https://blog.sciencenet.cn/blog-89075-238819.html
上一篇： Consequence-Driven Reasoning for Horn SHIQ Ontologies
下一篇：Structure and Interpretation of Computer Programs
