J4 ›› 2008, Vol. 30 ›› Issue (10): 67-68.
• 论文 • 上一篇 下一篇
王俐莉 王元元 张兴元
出版日期:
发布日期:
Online:
Published:
摘要：
本文针对命题演算形式系统，在机器辅助定理证明系统Isabelle／HOL中为其建立逻辑模型，并分别形式化验证了PC和ND的主要性质，以及完备性定理的证明。通过对PC和ND 的分析和验证表明，采用机器辅助定理证明系统，对以数理逻辑为平台的各种形式系统进行严格的分析和证明是可行的。
关键词: 命题演算形式系统 完备性定理 形式化验证 Isabelle／HOL／Isar
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.
Key words: propositional calculus form system, completeness theorem, formal verification, Isabelle/HOL/Isar
王俐莉 王元元 张兴元. 命题演算形式系统在Isabelle／HOL中的形式化[J]. J4, 2008, 30(10): 67-68.
0 / / 推荐
导出引用管理器 EndNote|Ris|BibTeX
链接本文: http://joces.nudt.edu.cn/CN/
http://joces.nudt.edu.cn/CN/Y2008/V30/I10/67
