定义3：设有公式集F=F1,F2,,F}若存在一个代 换入使得F12=F2入=.=Fn2,则称1为公式集F 的一个合一，且称F1,F2,,Fn是可合一的。 例：设有公式集F=P(x,y,f(b),P(a,g(x),z)},下式 是它的一个合一： 2={a/x,g(a)/y,f(g(a)/z} 定义4.设G是公式集F的一个合一，如果对任一个 合一0都存在一个代换儿，使得0=σ°入，则称 G是一个最一般的合一。 求最一般合一的算法： (1)令k=0,Fk=F,σkε。F是欲求其最一般合一的 公式集，是空代换 (2)若Fk只含一个表达式，则算法停止，其中σk就 是最一般合一定义3：设有公式集F={F1,F2,…,Fn}若存在一个代 换λ使得F1λ=F2λ=…=Fnλ,则称λ为公式集F 的一个合一，且称F1,F2,…,Fn是可合一的。 例：设有公式集F={P(x,y,f(b)),P(a,g(x),z)},下式 是它的一个合一： λ={a/x,g(a)/y,f(g(a))/z} 定义4.设σ是公式集F的一个合一，如果对任一个 合一都存在一个代换λ，使得 =σλ,则称 σ是一个最一般的合一。 求最一般合一的算法： (1)令k=0,Fk=F,σk=ε。F是欲求其最一般合一的 公式集，ε是空代换 (2)若Fk只含一个表达式，则算法停止，其中σk就 是最一般合一