Formalization of Propositional Calculus Form Systems in Isabelle/HOL
Xingyuan Zhang · Computer Engineering and Science · 2008
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.