许 明，开金宇，肖 蕾，3

(1.厦门理工学院计算机与信息工程学院，福建厦门361024;2.安阳师范学院计算机与信息工程学院，河南安阳455002;3.上海大学计算机工程与科学学院，上海200027)

形式化系统方法是一种对形式化系统中形式化语言按照计算规则运算的结果依据推理规则进行逻辑推理判断的方法.由三大部分组成.第1部分是形式化语言，由形式化语言的字符集中的字符按照一定的语法规则组成的合法字符串，即是形式化语言，也称合式公式，记为wff.第2部分是形式化系统的推理机制.形式化系统的推理机制由两部分组成，1)公理，不需要依据推理规则即可判断为合法的字符串，称为公理，记作Axioms;2)推理规则，推理规则用于操纵Axioms和(或)其他wffs产生新的合法字符串wffs.第3部分是对形式化系统中形式化语言的语义解释.对形式化语言的语义解释用于对无意义的形式化语言，即合式公式，赋予有意义的领域含义.对形式化语言的语义解释通常采用自然语言，自然语言不是一种完美的形式化语言，但由于其通用性，所以在对语义解释没有严格要求下，使用自然语言对语义进行解释.

形式化系统有两个重要的性质:1)完备性;2)一致性.

假设对于形式化系统F，存在一些形式化语言{f1，f2，f3，…，fn}，对这些形式化语言的解释为{I[f1]，I[f2]，I[f3]，…，I[fn]}.

如果从语义解释的角度出发，存在从序列I[f1]= .T.，I[f2]= .T.，…，I[fk]= .T.可以语义推出I[fn]=.T.的情况下，依据形式化系统的推理规则可以从序列f1，f2，…，fk语法推出 fn，称形式化系统F具有完备性.对完备性的……