(2)当取｛l
i
｝=｛Q(y)｝和｛m
i
｝=｛
～
Q(z)｝时，则可得到消解式:
A
B
C
D
E
F
G
上式中，
A B C D E F G
表示的答案为:
A
P［z,f(y)]∨
～
Q(z)∨Q(z)
B
P[x,f(A)]∨P[x,f(y)]∨
～
P［y,f(A)]
C
P[z,f(y)]∨Q(y)∨
～
Q(z)
D
P[x,f(y)]∨Q(y)∨
～
Q(z)
E
P[x,f(A),g(x)]∨P［x,f(y)]∨
～
P［z,f(A),g(z)]
F
P[y,f(y)]
G
P[x,f(A),g(x)]∨P[x,f(y)]∨
～
P［y,f(A),g(y)]
返回课堂