2.4.2 归结式
在谓词逻辑下求两个子句的归结式,和命题逻辑一样是消互补对,但需考虑变量的合一与置换。
设C
1
，C
2
是两个无公共变量的子句，L
1
，L
2
分别是C
1
，C
2
的文字，如果L
1
，～L
2
有mgu σ,则
(C
1
σ-{L
1
σ})∪(C
2
σ-{L
2
σ})
称作子句C
1
、C
2
的一个二元归结式，而L
1
，L
2
为被归结的文字。