歸結(jié)演繹推理的歸結(jié)策略廣度優(yōu)先策略支持集策略刪除策略單文字子句策略線性輸入策略祖先過(guò)濾策略歸結(jié)演繹推理的歸結(jié)策略廣度優(yōu)先策略支持集策略刪除策略單文字子1歸結(jié)反演系統(tǒng)面臨著大子句集而引起的演繹效率問(wèn)題。

若盲目地隨機(jī)選擇子句對(duì)進(jìn)行歸結(jié)，不僅要耗費(fèi)許多時(shí)間，而且還會(huì)因?yàn)闅w結(jié)出了許多無(wú)用的歸結(jié)式而過(guò)分?jǐn)U張了子句集，從而浪費(fèi)了時(shí)空，并降低了效率。

解決問(wèn)題的關(guān)鍵在于選擇有利于導(dǎo)致快速產(chǎn)生空子句的子句對(duì)進(jìn)行歸結(jié)。

歸結(jié)反演系統(tǒng)面臨著大子句集而引起的演繹效率問(wèn)題。若盲目地隨2歸結(jié)策略刪除策略：限制策略：通過(guò)刪除某些無(wú)用的子句來(lái)縮小歸結(jié)的范圍

通過(guò)設(shè)置選用條件對(duì)參與歸結(jié)的子句進(jìn)行種種限制，減少歸結(jié)的盲目性，如支持集、線性輸入、單文字子句優(yōu)先、祖先過(guò)濾等策略。

歸結(jié)策略刪除策略：限制策略：通過(guò)刪除某些無(wú)用的子句來(lái)縮小歸結(jié)3廣度優(yōu)先策略廣度優(yōu)先是一種窮盡子句比較的復(fù)雜搜索方法廣度優(yōu)先策略廣度優(yōu)先是一種窮盡子句比較的復(fù)雜搜索方法4廣度優(yōu)先的歸結(jié)過(guò)程：設(shè)初始子句集為S0,歸結(jié)過(guò)程如下：從S0出發(fā)，對(duì)S0中的全部子句作所有可能的歸結(jié)，得到第一層歸結(jié)式，把這些歸結(jié)式的集合記為S1。2.用S0中的子句與S1中的子句作所有可能的歸結(jié)，得到第二層歸結(jié)式，把這些歸結(jié)式的集合記為S2。3.用S0和S1中的子句與S2中的子句作所有可能的歸結(jié)，得到第三層歸結(jié)式，把這些歸結(jié)式的集合記為S3。如此繼續(xù),直到得到空子句。廣度優(yōu)先的歸結(jié)過(guò)程：設(shè)初始子句集為S0,歸結(jié)過(guò)程如下：從S05例：子句集S={I(x)R(x),I(a),R(x)L(y),L(a)}S:S0:R(a)I(x)L(x)I(x)R(x)I(a)R(x)L(y)L(a)R(a)S1:L(a)L(a)I(a)I(a)NIL廣度優(yōu)先策略歸結(jié)出了許多無(wú)用的子句，既浪費(fèi)時(shí)間，有浪費(fèi)空間。容易引起組合爆炸。P(A)例：子句集S={I(x)R(x),I(a),R(x)6當(dāng)問(wèn)題有解時(shí)，用廣度優(yōu)先策略歸結(jié)能保證找到最短路徑。因此，它是一種完備的歸結(jié)策略。當(dāng)問(wèn)題有解時(shí)，用廣度優(yōu)先策略歸結(jié)能保證找到最短路徑。因此，它7支持集策略要求每依次參加歸結(jié)的兩個(gè)親本子句中，至少應(yīng)該有一個(gè)是由目標(biāo)公式的否定所得到的子句或它們的后裔。支持集策略要求每依次參加歸結(jié)的兩個(gè)親本子句中，至少應(yīng)該有一個(gè)8支持集策略是完備的，即當(dāng)子句集不可滿足時(shí)，由支持集策略一定能夠歸結(jié)出一個(gè)空子句。支持集策略是完備的，即當(dāng)子句集不可滿足時(shí)，由支持集策略一定能9例：子句集S={I(x)R(x),I(a),R(x)L(y),L(a)}S:S0:R(a)I(x)L(x)I(x)R(x)I(a)R(x)L(y)L(a)S1:L(a)L(a)I(a)NILS3:例：子句集S={I(x)R(x),I(a),R(x)10刪除策略歸結(jié)時(shí)將無(wú)用的子句刪除掉，縮小搜索范圍，減少比較次數(shù)，從而提高歸結(jié)效率。刪除策略歸結(jié)時(shí)將無(wú)用的子句刪除掉，縮小搜索范圍，減少比較次數(shù)11常用的刪除方法：（1）純文字刪除法純文字：如果文字L在子句集中不存在與其互補(bǔ)的文字L，則稱該文字為純文字。例：對(duì)于子句集S={PQR,QR,Q,R}其中P為純文字，因此，PQR可從S中刪除。常用的刪除方法：（1）純文字刪除法純文字：如果文字L在子句集12（2）重言式刪除法重言式：如果一個(gè)子句中包含有互補(bǔ)的文字對(duì)，則稱該子句為重言式。例：P(x)P(x)、P(x)Q(x)P(x)（2）重言式刪除法重言式：如果一個(gè)子句中包含有互補(bǔ)的文字對(duì)，13（3）包孕刪除法例：P(x)包孕于P(y)Q(z)s={y/x}P(x)包孕于P(a)s={a/x}P(x)Q(z)包孕于P(f(x))Q(a)R(y)s={f(a)/x),a/z}設(shè)有子句C1和C2，如果存在一個(gè)置換s,使得C1sC2，則稱C1包孕于C2。（3）包孕刪除法例：設(shè)有子句C1和C2，如果存在一個(gè)置換s,14單文字子句策略要求每次參加歸結(jié)的兩個(gè)親本子句至少有一個(gè)子句是單文字子句單文字子句策略要求每次參加歸結(jié)的兩個(gè)親本子句至少有一個(gè)子句15單文字子句：如果一個(gè)子句只包含一個(gè)文字，則稱此子句為單文字子句。例：子句集S={I(x)R(x),I(a),R(x)L(y),L(a)}S:S0:R(a)I(x)R(x)I(a)R(x)L(y)L(a)R(a)NIL采用單文字子句策略，歸結(jié)式包含的文字?jǐn)?shù)將少于其親本子句中的文字?jǐn)?shù)，這將有利于向空子句的方向發(fā)展。但這種歸結(jié)策略是不完備的。即當(dāng)子句集為不可滿足時(shí)，用這種歸結(jié)策略不一定能歸結(jié)出空子句。單文字子句：如果一個(gè)子句只包含一個(gè)文字，則稱此子句為單文字子16線性輸入策略要求每次參加歸結(jié)的來(lái)年各個(gè)親本子句中，至少應(yīng)該有一個(gè)是初始子句集中的子句。線性輸入策略要求每次參加歸結(jié)的來(lái)年各個(gè)親本子句中，至少應(yīng)該有17例：子句集S={I(x)R(x),I(a),R(x)L(y),L(a)}S:S0:R(a)I(x)L(x)I(x)R(x)I(a)R(x)L(y)L(a)R(a)S1:I(a)L(a)L(a)I(a)NIL線性輸入策略可限制生成歸結(jié)式的數(shù)目，具有簡(jiǎn)單高效的優(yōu)點(diǎn)，但也是一種不完備的策略。例：子句集S={I(x)R(x),I(a),R(x)18例：子句集：S={Q(u)P(a),Q(w)P(w),Q(x)P(x),Q(y)P(y)}從S出發(fā)和容易找到一克歸結(jié)反演樹，卻不存在線性輸入策略的歸結(jié)反演樹。

例：子句集：S={Q(u)P(a),Q(w)19祖先過(guò)濾策略每次參加歸結(jié)的兩個(gè)親本子句，只要滿足以下兩個(gè)條件中的任意一個(gè)就可進(jìn)行歸結(jié)：（1）兩個(gè)親本子句中至少有一個(gè)是初始子句集中的子句。（2）如果兩個(gè)親本子句都不是初始子句集中的子句，則一個(gè)子句應(yīng)該是另一個(gè)子句的先輩子句。祖先過(guò)濾策略每次參加歸結(jié)的兩個(gè)親本子句，只要滿足以下兩個(gè)條件20例：子句集：S={Q(x)P(x),Q(y)P(y),

Q(w)P(w),Q(a)P(A)}用祖先過(guò)濾策略證明S為不可滿足。Q(x)P(x)Q(y)P(y)P(x)Q(w)P(w)Q(w)Q(a)P(A)P(A)NIL可以證明祖先過(guò)濾策略也是完備的。例：子句集：S={Q(x)P(x),Q(y21實(shí)際應(yīng)用中可以將幾種策略結(jié)合起來(lái)使用。在選擇歸結(jié)反演策略時(shí)，主要應(yīng)考慮其完備性和效率問(wèn)題。實(shí)際應(yīng)用中可以將幾種策略結(jié)合起來(lái)使用。在選擇歸結(jié)反演策略時(shí)，22作業(yè)1：設(shè)有子句集：{P(x)Q(x,b),P(a)Q(a,b),Q(a,f(a)),

P(x)Q(x,x)}，分別用各種歸結(jié)策略求出其歸結(jié)式。作業(yè)2：對(duì)子句集：{PQ,QR,RW,RP,WQ,QR}用線性輸入策略是否可證明該子句的不可滿足性？作業(yè)1：設(shè)有子句集：作業(yè)2：對(duì)子句集：{PQ,QR23作業(yè)2：對(duì)線性輸入策略和單文字策略分別舉一個(gè)反例，以說(shuō)明它們是不完備的。作業(yè)2：對(duì)線性輸入策略和單文字策略分別舉一個(gè)反例，以說(shuō)明它們24歸結(jié)演繹推理的歸結(jié)策略廣度優(yōu)先策略支持集策略刪除策略單文字子句策略線性輸入策略祖先過(guò)濾策略歸結(jié)演繹推理的歸結(jié)策略廣度優(yōu)先策略支持集策略刪除策略單文字子25歸結(jié)反演系統(tǒng)面臨著大子句集而引起的演繹效率問(wèn)題。

若盲目地隨機(jī)選擇子句對(duì)進(jìn)行歸結(jié)，不僅要耗費(fèi)許多時(shí)間，而且還會(huì)因?yàn)闅w結(jié)出了許多無(wú)用的歸結(jié)式而過(guò)分?jǐn)U張了子句集，從而浪費(fèi)了時(shí)空，并降低了效率。

解決問(wèn)題的關(guān)鍵在于選擇有利于導(dǎo)致快速產(chǎn)生空子句的子句對(duì)進(jìn)行歸結(jié)。

歸結(jié)反演系統(tǒng)面臨著大子句集而引起的演繹效率問(wèn)題。若盲目地隨26歸結(jié)策略刪除策略：限制策略：通過(guò)刪除某些無(wú)用的子句來(lái)縮小歸結(jié)的范圍

通過(guò)設(shè)置選用條件對(duì)參與歸結(jié)的子句進(jìn)行種種限制，減少歸結(jié)的盲目性，如支持集、線性輸入、單文字子句優(yōu)先、祖先過(guò)濾等策略。

歸結(jié)策略刪除策略：限制策略：通過(guò)刪除某些無(wú)用的子句來(lái)縮小歸結(jié)27廣度優(yōu)先策略廣度優(yōu)先是一種窮盡子句比較的復(fù)雜搜索方法廣度優(yōu)先策略廣度優(yōu)先是一種窮盡子句比較的復(fù)雜搜索方法28廣度優(yōu)先的歸結(jié)過(guò)程：設(shè)初始子句集為S0,歸結(jié)過(guò)程如下：從S0出發(fā)，對(duì)S0中的全部子句作所有可能的歸結(jié)，得到第一層歸結(jié)式，把這些歸結(jié)式的集合記為S1。2.用S0中的子句與S1中的子句作所有可能的歸結(jié)，得到第二層歸結(jié)式，把這些歸結(jié)式的集合記為S2。3.用S0和S1中的子句與S2中的子句作所有可能的歸結(jié)，得到第三層歸結(jié)式，把這些歸結(jié)式的集合記為S3。如此繼續(xù),直到得到空子句。廣度優(yōu)先的歸結(jié)過(guò)程：設(shè)初始子句集為S0,歸結(jié)過(guò)程如下：從S029例：子句集S={I(x)R(x),I(a),R(x)L(y),L(a)}S:S0:R(a)I(x)L(x)I(x)R(x)I(a)R(x)L(y)L(a)R(a)S1:L(a)L(a)I(a)I(a)NIL廣度優(yōu)先策略歸結(jié)出了許多無(wú)用的子句，既浪費(fèi)時(shí)間，有浪費(fèi)空間。容易引起組合爆炸。P(A)例：子句集S={I(x)R(x),I(a),R(x)30當(dāng)問(wèn)題有解時(shí)，用廣度優(yōu)先策略歸結(jié)能保證找到最短路徑。因此，它是一種完備的歸結(jié)策略。當(dāng)問(wèn)題有解時(shí)，用廣度優(yōu)先策略歸結(jié)能保證找到最短路徑。因此，它31支持集策略要求每依次參加歸結(jié)的兩個(gè)親本子句中，至少應(yīng)該有一個(gè)是由目標(biāo)公式的否定所得到的子句或它們的后裔。支持集策略要求每依次參加歸結(jié)的兩個(gè)親本子句中，至少應(yīng)該有一個(gè)32支持集策略是完備的，即當(dāng)子句集不可滿足時(shí)，由支持集策略一定能夠歸結(jié)出一個(gè)空子句。支持集策略是完備的，即當(dāng)子句集不可滿足時(shí)，由支持集策略一定能33例：子句集S={I(x)R(x),I(a),R(x)L(y),L(a)}S:S0:R(a)I(x)L(x)I(x)R(x)I(a)R(x)L(y)L(a)S1:L(a)L(a)I(a)NILS3:例：子句集S={I(x)R(x),I(a),R(x)34刪除策略歸結(jié)時(shí)將無(wú)用的子句刪除掉，縮小搜索范圍，減少比較次數(shù)，從而提高歸結(jié)效率。刪除策略歸結(jié)時(shí)將無(wú)用的子句刪除掉，縮小搜索范圍，減少比較次數(shù)35常用的刪除方法：（1）純文字刪除法純文字：如果文字L在子句集中不存在與其互補(bǔ)的文字L，則稱該文字為純文字。例：對(duì)于子句集S={PQR,QR,Q,R}其中P為純文字，因此，PQR可從S中刪除。常用的刪除方法：（1）純文字刪除法純文字：如果文字L在子句集36（2）重言式刪除法重言式：如果一個(gè)子句中包含有互補(bǔ)的文字對(duì)，則稱該子句為重言式。例：P(x)P(x)、P(x)Q(x)P(x)（2）重言式刪除法重言式：如果一個(gè)子句中包含有互補(bǔ)的文字對(duì)，37（3）包孕刪除法例：P(x)包孕于P(y)Q(z)s={y/x}P(x)包孕于P(a)s={a/x}P(x)Q(z)包孕于P(f(x))Q(a)R(y)s={f(a)/x),a/z}設(shè)有子句C1和C2，如果存在一個(gè)置換s,使得C1sC2，則稱C1包孕于C2。（3）包孕刪除法例：設(shè)有子句C1和C2，如果存在一個(gè)置換s,38單文字子句策略要求每次參加歸結(jié)的兩個(gè)親本子句至少有一個(gè)子句是單文字子句單文字子句策略要求每次參加歸結(jié)的兩個(gè)親本子句至少有一個(gè)子句39單文字子句：如果一個(gè)子句只包含一個(gè)文字，則稱此子句為單文字子句。例：子句集S={I(x)R(x),I(a),R(x)L(y),L(a)}S:S0:R(a)I(x)R(x)I(a)R(x)L(y)L(a)R(a)NIL采用單文字子句策略，歸結(jié)式包含的文字?jǐn)?shù)將少于其親本子句中的文字?jǐn)?shù)，這將有利于向空子句的方向發(fā)展。但這種歸結(jié)策略是不完備的。即當(dāng)子句集為不可滿足時(shí)，用這種歸結(jié)策略不一定能歸結(jié)出空子句。單文字子句：如果一個(gè)子句只包含一個(gè)文字，則稱此子句為單文字子40線性輸入策略要求每次參加歸結(jié)的來(lái)年各個(gè)親本子句中，至少應(yīng)該有一個(gè)是初始子句集中的子句。線性輸入策略要求每次參加歸結(jié)的來(lái)年各個(gè)親本子句中，至少應(yīng)該有41例：子句集S={I(x)R(x),I(a),R(x)L(y),L(a)}S:S0:R(a)I(x)L(x)I(x)R(x)I(a)R(x)L(y)L(a)R(a)S1:I(a)L(a)L(a)I(a)NIL線性輸入策略可限制生成歸結(jié)式的數(shù)目，具有簡(jiǎn)單高效的優(yōu)點(diǎn)，但也是一種不完備的策略。例：子句集S={I(x)R(x),I(a),R(x)42例：子句集：S={Q(u)P(a),Q(w)P(w),Q(x)P(x),Q(y)P(y)}從S出發(fā)和容易找到一克歸結(jié)反演樹，卻不存在線性輸入策略的歸結(jié)反演樹。

例：子句集：S={Q(u)P(a),Q(w)43祖先過(guò)濾策略每次參加歸結(jié)的兩個(gè)親本子句，只要滿足以下兩個(gè)條件中的任意一個(gè)就可進(jìn)行歸結(jié)：（1）兩個(gè)親本子句中至