文档介绍：(补充)(补充)(补充)(补充)(补充):谓词逻辑的基本知识合一算法(求最一般的一致置换或合一者mgu)本节:消解原理(或者归结原理),作为合一算法的输入(公式集)(Skolem)范式4子句集设α,β是一个谓词公式,将量词记作θ(即或)1自由变元与约束变元如果α中包含部分公式(θx)β,则β中变元x的一切出现都称为x在α中的约束出现,相应地称x为约束变元(哑元、虚构变量、约束变量)约束变元α中不在任何量词作用域内的变元x,称为变元x在α中的自由出现,相应地称x为自由变元(自由变量)自由变元:量词的作用域(辖域)是直接跟在它后面的公式如果有括号,则是括号里的公式如果没有括号,则是最短的完整公式说明: