数理逻辑证明检查模块 Overview 1. 推理成分 前提,可能是若干个命题 结论,一个(一个命题) 推理序列 2. 推理过程 按照规则不断增加推理序列(用一个字符串的形式表示),只有合理的字符串能够加入，不合理的加入失败 直到结论出现,证明完成 3. 字符串格式约定 可以有任意个空格(空格会自动消去) PC 检查 propositional calculus 1. ND 检查