命题演算形式系统在Isabelle/HOL中的形式化

• 作者: 张兴元 王俐莉 王元元
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 命题演算形式系统 完备性定理 形式化验证 Isabelle/HOL/Isar
• 年，卷（期）: 2008,（10）
• 所属期刊栏目: 离散数学理论与应用
• 页码范围: 67-68,89
• 页数: 3页
• 分类号: TP311
• 字数: 2576字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2008.10.023

摘要

本文针对命题演算形式系统,在机器辅助定理证明系统Isabelle/HOL中为其建立逻辑模型,并分别形式化验证了PC和ND的主要性质,以及完备性定理的证明.通过对PC和ND的分析和验证表明,采用机器辅助定理证明系统,对以数理逻辑为平台的各种形式系统进行严格的分析和证明是可行的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王元元	解放军理工大学指挥自动化学院	46	351	12.0	16.0
2	张兴元	解放军理工大学指挥自动化学院	14	20	2.0	3.0
3	王俐莉	解放军理工大学指挥自动化学院	6	10	2.0	3.0