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

摘要：

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

关键词：命题演算形式系统、完备性定理、形式化验证、Isabelle/HOL/Isar

所属期刊栏目：30

分类号：TP311(计算技术、计算机技术)

在线出版日期：2008-12-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：67-68,89