定理3(合一定理)、如果S是一个非空有限可合一的 公式集,则合一算法总是在步(2)停止,且最后 的σ即是S的最一般合一
定理3（合一定理）、如果S是一个非空有限可合一的 公式集，则合一算法总是在步（2）停止，且最后 的k即是S的最一般合一
3.2.4谓词逻辑中的归结原理 定义12、设C1,C2是两个没有相同变元的子句,L1 2分别是C1,C2中的两个文字,如果L与—L2有最一般 合σ,则子句C12=C10{L1o(C20{L2}),称作 C1和C2的二元归结式(二元消解式)。C1和C2称为C12 的亲本子句,L1,L2称为消解文字。 数若在参加归结的子句内部含有可合一文字,则在进行 归结之前,应对这些文字进行合一。 定义13、如果子句C中,两个或两个以上的文字有一个 最一般合一σ,则称Co为C的因子
3.2.4 谓词逻辑中的归结原理 定义12、设C1，C2是两个没有相同变元的子句，L1， L2分别是C1，C2中的两个文字，如果L1与L2有最一般 合一 ，则子句C12=(C1-{L1}) (C2-{L2})，称作 C1和C2的二元归结式（二元消解式）。 C1和C2称为C12 的亲本子句， L1，L2称为消解文字。 若在参加归结的子句内部含有可合一文字，则在进行 归结之前，应对这些文字进行合一。 定义13、如果子句C中，两个或两个以上的文字有一个 最一般合一 ，则称C为C的因子