23
第4章 消解法
mgu求解例子(1)
• 例1:求W={P(a, x, f(g(y))), P(z, f(a), f(u))}的 mgu
(1)0=,W0=W,D0={a, z} (2)1=0{a/z}={a/z},W1= W01={P(a, x, f(g(y))), P(a, f(a), f(u))},D1={x, f(a)} (3)2=1{f(a)/x}={a/z, f(a)/x},W2= W12= {P(a, f(a), f(g(y))), P(a, f(a), f(u))},D2={g(y), u} (4)3=2{g(y)/u}={a/z, f(a)/x, g(y)/u} , W3= W23= {P(a, f(a), f(g(y))), P(a, f(a), f(g(y)))}, D3= 此时W已合一,mgu=3={a/z, f(a)/x, g(y)/u} ★
6
第4章 消解法
基本思想(2)
• 这样,在证假(不可满足)的意义上使公 式与子句集的语义解释等价、并与H解释 等价,作为消解法的开端 • 引入语义树,让所有解释都展现在语义 树上,以便找到H解释。 • 最后在改进寻找解释算法的复杂性中发 现了消解式,从而构成了消解法的完整 理论基础 • 消解也叫归结,本章混用这两个称呼
7
第4章 消解法
4.2 消解法
4.2.1 公式到子句集的转换 4.2.2 合一算法 4.2.3 消解式 4.2.4 消解法的实施
第4章 消解法
消解法的形式
• 消解法举例:
P S P Q ( P Q)
• 此时只要使用单文字删除规则就可以推 出结论Q。但是如果子句中包含变量,则 常常必须经过变量置换才能进行消解
12