高级人工智能.Modus Pones定理完备性证明（详细）
写在最前
本文为博主复习高级人工智能这门课程时，针对于Modus Pones定理完备性证明这一问题，所做的笔记。这是国科大本门课程的必考题，步骤较为详细，建议理解后记忆。
Modus Pones定理回顾
命题演算分离规则（Modus Pones规则）是命题演算或谓词演算的公理系统的一个变形规则， 其具体内容是：若A→B是可推出的，并且A也是可推出的，则B也是可推出的。若用“⊢"表示“可推出的”，可表述为： 若⊢A并且⊢A→B，则⊢B。这里的A、 B是表示任一合式公式的元语言符号； “⊢”表示紧跟其后的公式为本系统所肯定，即为本系统的定理。即是说，如果A→B 和A都是系统中的定理，则B也是系统中的定理。
这条规则可以表示为：
这条规则实质上就是承认前件则必须承认后件的充分条件假言推理。
证明过程
若证明Modus Pones定理，即证明：若KB|=α，则 KB⊢ α，
此时KB仅包含Horn子句，⊢仅使用Modus Pones定理，且α是一个正文字。
设RC(KB)是KB使用Modus Pones规则推导出的所有子句的集合。
我们构造如下真值指派m：对任意symbol a，当且仅当a∈RC(KB)时将a指派为True。
接下来我们证明在m下KB为真。
假设在m下KB为假，则必存在一个Horn子句，该子句在m下为假。
- 若子句为a1 ∧ a2 ∧ … ∧ ak => b，此时a1，a2，… ，ak均为True，b为False，根据定义，ai∈RC(KB)。根据Modus Pones规则，b∈RC(KB)，因此b在m下被指派为True，矛盾。
- 若子句为b，则在m下b为False，这与b∈RC(KB)矛盾。
综上，在m下KB为真。
因此，若KB|=α，在m下α必然为真，故α∈RC(KB)，即KB⊢ α得证。