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

发布时间：2021-06-17 10:14

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

【文章来源】：计算机工程与科学. 2008,(10)北大核心

【文章页数】：3 页

【文章目录】：
1 引言
2 命题演算形式系统PC
    2.1 PC的基本构成
    2.2 系统内的推理
        2.2.1 命题公式的真值
        2.2.2 证明和演绎
3 完备性定理的证明
4 命题演算形式系统ND
5 结束语



本文编号：3235003