| 命题演算形式系统在Isabelle／HOL中的形式化 |
| |
| 引用本文： | 王俐莉,王元元,张兴元. 命题演算形式系统在Isabelle／HOL中的形式化[J]. 计算机工程与科学, 2008, 30(10): 67-68 |
| |
| 作者姓名： | 王俐莉 王元元 张兴元 |
| |
| 作者单位： | 解放军理工大学指挥自动化学院,江苏,南京,210007 |
| |
| 摘 要： | 本文针对命题演算形式系统，在机器辅助定理证明系统Isabelle／HOL中为其建立逻辑模型，并分别形式化验证了PC和ND的主要性质，以及完备性定理的证明。通过对PC和ND的分析和验证表明，采用机器辅助定理证明系统，对以数理逻辑为平台的各种形式系统进行严格的分析和证明是可行的。
|
| 关 键 词： | 命题演算形式系统 完备性定理 形式化验证 Isabelle／HOL／Isar |
Formalization of Propositional Calculus Form Systems in Isabelle/HOL |
| |
| WANG Li-li,WANG Yuan-yuan,ZHANG Xing-yuan. Formalization of Propositional Calculus Form Systems in Isabelle/HOL[J]. Computer Engineering & Science, 2008, 30(10): 67-68 |
| |
| Authors: | WANG Li-li WANG Yuan-yuan ZHANG Xing-yuan |
| |
| Abstract: | This paper aims at propositional calculus form systems,builds a logical model in Isabelle/HOL,and verifies the main properties of PC and ND.It also proves the completeness theorem.Analysis and verification of PC and ND shows that in a machine-assisted verification system,a stringent analysis and proof of various formal systems based on mathematical logic is feasible. |
| |
| Keywords: | propositional calculus form system completeness theorem formal verification Isabelle/HOL/Isar |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 |
|
点击此处可从《计算机工程与科学》下载免费的PDF全文 |
