人工智能原理

Agenda3.1引言3.2命題邏輯中的歸結(jié)原理3.3謂詞邏輯中的歸結(jié)原理3.1Introduction證明的基本思想是：設F1、…、Fn、G為公式，G為F1、…、Fn的邏輯推論，當且僅當公式（（F1

…

Fn）

G）是有效的

也可以采用反證法的思想：設F1、…、Fn、G為公式，G為F1、…、Fn的邏輯推論，當且僅當公式（F1

…

Fn

G）是不可滿足的

歸結(jié)法的本質(zhì)上就是一種反證法，它是在歸結(jié)推理規(guī)則的基礎上實現(xiàn)的：為了證明一個命題P恒真，它證明其反命題～P恒假，即不存在使得

P為真的解釋

3.2命題邏輯中的歸結(jié)原理3.2.1子句和子句形3.2.2歸結(jié)

3.2.3歸結(jié)反演3.2.4合理性和完備性3.2.5歸結(jié)反演的搜索策略3.2.1子句和子句形（1）文字是原子或其否定子句是文字的析取完備連接符集合：合取范式（CNF）（L11…L1n1)…(Lm1…Lmnm)析取范式（DNF）（L11…L1n1)…(Lm1…Lmnm)定理：對任意公式，都有與之等值的合取范式和析取范式轉(zhuǎn)換方法：一般方法真值表方法3.2.2子句和子句形（2）一般方法EliminateimplicationsignsbyusingtheequivalentformusingReducethescopesof~signsbyusingDeMorgan’slawandbyeliminatingdouble~signsConverttoCNFbyusingtheassociativeanddistributivelaws.3.2.2Resolution

對任意三個子句p、q和rpr,q~rpq

或者：forC1=PC1’,C2=~PC2’PC1’,~PC2’C1’C2’歸結(jié)式：R(C1,C2)=C1’C2’證明：3.2.3ResolutionRefutations（1）定理證明的任務:由前提A1A2...An推出結(jié)論B即證明:A1A2...AnB永真轉(zhuǎn)化為證明:A1A2...An~B為永假式歸結(jié)推理就是:從A1A2...An~B出發(fā),使用歸結(jié)推理規(guī)則來找出矛盾,最后證明定理A1A2...AnB的成立來自

中國最大的資料庫下載3.2.3ResolutionRefutations（2）歸結(jié)方法是一種機械化的,可在計算機上加以實現(xiàn)的推理方法可認為是一種反向推理形式提供了一種自動定理證明的方法3.2.3ResolutionRefutations（3）一般過程:建立子句集S從子句集S出發(fā),僅對S的子句間使用歸結(jié)推理規(guī)則如果得出空子句,則結(jié)束;否則轉(zhuǎn)下一步將所得歸結(jié)式仍放入S中對新的子句集使用歸結(jié)推理規(guī)則轉(zhuǎn)(3)空子句不含有文字,它不能被任何解釋滿足,所以空子句是永假的,不可滿足的歸結(jié)過程出現(xiàn)空子句,說明出現(xiàn)互補子句對,說明S中有矛盾,因此S是不可滿足的.3.2.3ResolutionRefutations（4）例子:證明(P

Q)

~Q

~p首先建立子句集:(PQ)~Q~(~P)(~PQ)~QPS={~PQ,~Q,P}對S作歸結(jié):(1)~PQ(2)~Q(3)P(4)~P(1)(2)歸結(jié)(5)(3)(4)歸結(jié)3.2.4SoundnessandCompleteness歸結(jié)原理是合理的歸結(jié)原理是完備的3.2.5ResolutionRefutationSearchStrategies

有序策略（Orderstrategies）Refinementstrategies支持集（Setofsupport）:每次歸結(jié)時，參與歸結(jié)的子句中至少應有一個是由目標公式的否定所得到的子句，或者是它們的后裔該策略是完備的線性輸入（LinearInput）：參與歸結(jié)的