【正文】 可能消去，因此，包含它的子句進(jìn)行歸結(jié)時(shí)不可能得到空子句，即這樣的子句對(duì)歸結(jié)是無意義的，所以，這樣的子句從子句集中刪除。（請(qǐng)給出純文字刪除的算法實(shí)現(xiàn)） ? （ 2）重言式刪除法 ? 如果一個(gè)子句中同時(shí)包含互補(bǔ)文字對(duì)，則稱該子句為重言式，顯然重言式不會(huì)影響子句集合 S的不可滿足性，所以，可以從子句集合中刪除。（給出檢查一個(gè)公式是否是重言式的算法實(shí)現(xiàn)） ? （ 3）包孕刪除法（被歸類的子句可以刪除） ? 設(shè)有子句 C1和 C2， 如果存在代換 ?，使得 C1 ?? C2，則稱 C1包孕于 C2或說 C2包孕 C1， 包的子句可以刪除，即 62 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 (續(xù)） ? 子句 C2可以刪除。（想一想它的原理是什麼？ ? P?（ P??Q） =P） ? 支持集策略 ? 每次歸結(jié)時(shí)，親本子句中至少應(yīng)有一個(gè)是由目標(biāo)公式的否定所得到的子句，或者是它們的后裔。例如有子句集合 S={?I(x) ? R(x), I(a), ?R(y)? ?L(y), L(a)} ? 其中 ?I(x) ? R(x)是目標(biāo)公式的否定得到的子句。用支持集歸結(jié)的過程是： ? S:（ 1） ?I(x) ? R(x) ? (2) I(a) ? (3) ?R(y) ? ?L(y) ? (4) L(a) ? S1 (5) R(a) (1)與（ 2）歸結(jié) 63 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 (續(xù)） ? (6) ?I(x) ? ?L(x) S2 (1)與（ 3）歸結(jié) ? S2 : (7) ?L(a) (2)與（ 6）歸結(jié) ? (8) ?L(a) (3)與（ 5）歸結(jié) ? (9) ?I(a) (4)與（ 6）歸結(jié) ? S3: (10) NIL (2)與（ 9）歸結(jié) ? 上述歸結(jié)過程可以用 P141頁的圖 410來描述。 ? 線性輸入策略 ? 線性歸結(jié)是這樣一種歸結(jié)，首先從子句集中選取一個(gè)稱為頂子句的子句 C0 開始做歸結(jié)，其次是歸結(jié)過程中所得到的歸結(jié)式 Ci立即同另一子句 Bi進(jìn)行歸結(jié)得歸結(jié)式 Ci+1。 而 Bi?S ? Ck(ki) (已出現(xiàn)過的歸結(jié)式）。這里關(guān)鍵的問題是頂子句的選擇，一般選擇結(jié)論的否定作為頂子句。 64 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 (續(xù)） ? 例如：證明 P ?Q， ? P ?Q， P ? ? Q ? P ?Q ? 解，問題轉(zhuǎn)化成證子句集合 S={P ?Q， ? P ?Q， P ? ? Q ， ? P ? ? Q} 的不可滿足問題，用線形消解的圖解表示如下： PvQ~PvP~QPv~Q~Pv~65 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 (續(xù)） ? 單文字子句策略 ? 如果一個(gè)子句只包含一個(gè)文字，則稱它為單文字子句。 ? 單文字子句策略要求參加歸結(jié)的兩個(gè)子句中必須至少有一個(gè)是單文字子句。例子見 P142頁的例 文字策略是不完備的，即當(dāng)子句集合中不存在單文字子句時(shí)，不能使用單文字子句策略。 ? 祖先過濾形策略 ? 該策略與線性輸入策略比較相似，它要求對(duì)兩個(gè)子句進(jìn)行消解時(shí)，只要它們滿足下面兩個(gè)條件之一就可進(jìn)行歸結(jié)。 ? （ 1） C1與 C2中至少有一個(gè)是初始子句集中的子句。 ? （ 2）如果兩個(gè)子句都不是初始子句集中的子句，則一個(gè)應(yīng)是另一個(gè)的祖先。所謂 C1是 C2的祖先是指 C2是由 C1和其它子句消解得到的消解式。 66 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 (續(xù)） ? 例 S={~P(x)vQ(x),~P(y)v~Q(y),P(u)vQ(u), P(t)v~Q(t)} ? 歸結(jié)過程如下圖所示： ~Q(x)P(t)v~Q(t)P(u)~P(x)VQ(x)~P(x)vQ(x)~P(y)v~Q(y)~P(x)P(u)vQ(u)NIL67 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 (續(xù)） ? 以上我們討論了歸結(jié)演繹推理，它是在定理自動(dòng)證明中影響較大的一種推理方法。它的缺點(diǎn)是要求把謂詞公式轉(zhuǎn)化成子句集，不便于理解，另外它還可能會(huì)丟失一些重要的控制信息。 ? 針對(duì)歸結(jié)演繹存在的上述問題，人們提出了多種非子句定理證明的方法，尼爾遜提出的基于與 /或形的演繹推理就是其中的一種。 68 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 與 /或形演繹推理 ? 歸結(jié)演繹要求把相關(guān)問題的知識(shí)及問題的否定均轉(zhuǎn)化成子句形式，然后通過歸結(jié)演繹推理，其推理規(guī)則只有一條，即歸結(jié)規(guī)則。與 /或形演繹推理則是把領(lǐng)域知識(shí)及已知事實(shí)分別用蘊(yùn)含式及與 /或形表示出來，然后通過運(yùn)用蘊(yùn)含式進(jìn)行演繹推理，從而證明某個(gè)目標(biāo)公式。 ? 與 /或形演繹推理分別分為正向演繹、逆向演繹及雙向演繹三種推理形式，下面分別介紹它們。 ? /或形正向演繹推理 ? 在這種推理中，對(duì)已知事實(shí)、 F規(guī)則及目標(biāo)公式的表示形式都有一定的要求，如果不滿足要求的形式就需要變換。 69 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 與 /或形演繹推理 ? 事實(shí)表達(dá)式的與 /或形變換及其樹形表示 ? 變換過程與化子句集類似，只是不必化為子句的合取形式，也不消去公式中的合取詞。 ? F規(guī)則的表示形式 ? 在與 /或形正向演繹推理中，通常要求 F規(guī)則具有如下的形式： ? L?W ? 其中， L是單文字， W是與 /或形。 ? 之所以要求 F規(guī)則的左部為單文字，是因?yàn)樵谶M(jìn)行演繹推理時(shí)，要用 F規(guī)則作用于表示事實(shí)的與 /或樹，而該與 /或樹的葉節(jié)點(diǎn)都是單文字，這樣就可以用 F規(guī)則的左部與葉節(jié)點(diǎn)進(jìn)行簡(jiǎn)單匹配（合一）。 70 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 與 /或形演繹推理 ? 如果領(lǐng)域知識(shí)不是上面的形式則通過等價(jià)變換變成規(guī)定的形式。例如對(duì)公式 ? （ ?x)(((?y)((?z)P(x,y,z))? (?u)Q(x,u))? ? （ ?x)( ~ ((?y)((?z)P(x,y,z))? (?u)Q(x,u)) ? ? (?x)( (?y) (?z) ~ P(x,y,z) ? (?u)Q(x,u)) ? ? (?x) (?y) (?z) (?u)(~ P(x,y,z) ? Q(x,u)) ? ? (?u)(~ P(x,y,f(x,y)) ? Q(x,u)) ? ? ~ P(x,y,f(x,y)) ? Q(x,u) ? P(x,y,f(x,y)) ? Q(x,u) 71 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 與 /或形演繹推理 ? 目標(biāo)公式的表示形式 ? 在與 /或形正向推理中，要求目標(biāo)公式用子句表示，否則就需要化成子句形式，轉(zhuǎn)化方法同前。 ? 推理過程 ? 應(yīng)用 F規(guī)則進(jìn)行推理的目的在于證明某個(gè)目標(biāo)公式。如果從已知事實(shí)的與 /或樹出發(fā)，通過運(yùn)用 F規(guī)則最終推出了欲證明的目標(biāo)公式，則推理就可成功結(jié)束。其推理過程如下： ? (1)首先用與 /或樹把已知事實(shí)表示出來； ? (2)用 F規(guī)則的左部和與 /或樹的葉節(jié)點(diǎn)進(jìn)行匹配，并將匹配成功的 F規(guī)則加入到與 /或樹中； ? (3)重復(fù)第 (2)步，直到產(chǎn)生一個(gè)含有目標(biāo)節(jié)點(diǎn)作為終止節(jié)點(diǎn)的解圖為止。 72 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 與 /或形演繹推理（續(xù)） ? 設(shè)已知的事實(shí)為 AVB ? F規(guī)則為： ? r1: A?C?D ? R2:B?E?G ? 欲證明的目標(biāo)公式為： ? CVG ? 其證明過程如右圖所示 r2r1目標(biāo)匹配F規(guī) 則匹配已知事實(shí)AAVBBA BGEDCC G73 2022/5/30 鄭州大學(xué)振動(dòng)工程研究所 與 /或形演繹推理（續(xù)） ? 上圖中已知事實(shí)為 AVB ? F規(guī)則為： r1:A?C?D ? r2:B?E?G ? 欲證明的目標(biāo)公式為 ? C ?G