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

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

单位：解放军理工大学指挥自动化学院 江苏南京210007