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

Abstract:

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.

Key words: propositional calculus form system, completeness theorem, formal verification, Isabelle/HOL/Isar