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

Formalization of Propositional Calculus Form Systems in Isabelle/HOL

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

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.