代數(shù)等式理論的自動定理證明計算機(jī)科學(xué)導(dǎo)論第一講

1、代數(shù)等式理論的自動定理證明計算機(jī)科學(xué)導(dǎo)論第一講,計算機(jī)科學(xué)技術(shù)學(xué)院陳意云0551-63607043, yiyun@ustc.edu.cnhttp://staff.ustc.edu.cn/~yiyun/,課 程 內(nèi) 容,課程內(nèi)容圍繞學(xué)科理論體系中的模型理論, 程序理論和計算理論1. 模型理論關(guān)心的問題 給定模型M，哪些問題可以由模型M解決；如何比較模型的表達(dá)能力2. 程序理論關(guān)心的問題給定模型M，如何用模型M解決問題

2、包括程序設(shè)計范型、程序設(shè)計語言、程序設(shè)計、形式語義、類型論、程序驗證、程序分析等3. 計算理論關(guān)心的問題給定模型M和一類問題, 解決該類問題需多少資源,本次講座基于中學(xué)的等式推理,與這些內(nèi)容關(guān)系不大,2,課 程 內(nèi) 容,本講座內(nèi)容以代數(shù)等式理論中的定理證明為例，介紹怎樣從中學(xué)生熟知的等式演算方法，構(gòu)造等式定理的自動證明系統(tǒng)，即將問題變?yōu)榭捎糜嬎銠C(jī)求解有助于理解計算思維的含義計算思維（譯文） 運(yùn)用計算機(jī)科學(xué)的基礎(chǔ)概念進(jìn)

3、行問題求解、系統(tǒng)設(shè)計、以及人類行為理解等涵蓋計算機(jī)科學(xué)之廣度的一系列思維活動,3,講 座 提 綱,基本知識代數(shù)項、代數(shù)等式、演繹推理規(guī)則、代數(shù)等式理論、等式定理證明方法項重寫系統(tǒng)終止性、良基關(guān)系、合流性、局部合流性、關(guān)鍵對良基歸納法僅舉例說明Knuth-Bendix完備化過程也僅舉例說明,4,基 本 知 識,代數(shù)項和代數(shù)等式（僅涉及一個類型）代數(shù)項例：自然數(shù)類型nat 0, 1, 2, … :

4、nat常量 x, y : nat變量 +, f : nat ? nat ? nat 二元函數(shù) S : nat ? nat一元的后繼函數(shù) 0, x, x + 1, x + S(y)和f(100, y) 都是代數(shù)項代數(shù)等式例： x + 0 = x，x + S(y) = S(x + y) x + y = z + 5,5,基

5、 本 知 識,代數(shù)項和代數(shù)等式（涉及多個類型）例：定義有限表：同類數(shù)據(jù)的有限序列的集合 ? 6, 17, 50, 28, 188, 92, 30, 67, 15 ? 18.8, 9.2, 50, 77, 8.6, 5.5, 40.0 ? a, b, c, d, e, f, …, z（非數(shù)值數(shù)據(jù)）上述數(shù)據(jù)涉及兩個類型 ? 序列中元素的類型 — 數(shù)值或非數(shù)值類型 ? 這些序列所屬的類

6、型，稱為表（list）類型 —非數(shù)值類型中學(xué)所學(xué)的代數(shù)概念在此已經(jīng)擴(kuò)展,6,基 本 知 識,代數(shù)項和代數(shù)等式（涉及多個類型）代數(shù)項（表類型list ，表元類型atom） ? x : atom,l : list 變量 ? nil : list 零元構(gòu)造函數(shù) (常量) ? cons : atom ? list ? list 構(gòu)造

7、函數(shù) ? first : list ? atom，rest : list ? list 觀察函數(shù) ? nil, cons(x, l), rest(cons(x, nil)), rest(cons(x, l)), cons(first(l), rest(l))都是代數(shù)項。用T 表示項集代數(shù)等式(方括號列出等式中出現(xiàn)的變量及類型) first(cons(x, l)) = x [x : atom,

8、 l : list] rest(cons(x, l)) = l [x : atom, l : list],7,基 本 知 識,等式證明例：基于一組等式（公式、公理）：x + 0 = x 和 x + S(y) = S(x + y) 怎么證明等式：x + S(S(y)) = S(S(x + y)) ?需要有推理規(guī)則,8,等式證明的演繹推理規(guī)則自反公理：M ? M ???對稱規(guī)則：傳遞

9、規(guī)則：加變量規(guī)則：等價代換規(guī)則：,基 本 知 識,x不在?中,P , Q 是類型s的項,9,等式推理的例子等價代換規(guī)則：等式公理：x + 0 = x和x + S(y) = S(x + y)證明等式： x + S(S(y)) = S(S(x + y))證明: x + S(S(y)) 根據(jù)x + S(z) = S(x + z)，S(y) = S(y)=S(x + S(y))使用等價代換規(guī)則得到第一個等式 S(x +

10、 S(y)) 根據(jù)S(z) = S(z)，x + S(y) = S(x + y)= S(S(x + y)) 使用等價代換規(guī)則得到第二個等式x + S(S(y)) = S(S(x + y)) 根據(jù)傳遞規(guī)則和上面兩等式,基 本 知 識,10,等式推理的例子等價代換規(guī)則：等式公理：x + 0 = x和x + S(y) = S(x + y)證明等式： x + S(S(y)) = S(S(x + y))證明: x + S

11、(S(y))=S(x + S(y)) 我們的證明演算習(xí)慣見左邊= S(S(x + y)) 它是基于剛才所介紹的演繹推理的若希望計算機(jī)來自動推理，嚴(yán)格的推理規(guī)則是必須提供的,基 本 知 識,11,基 本 知 識,代數(shù)等式理論（algebraic equation theory）在項集T 上從一組等式E（公理）能推出的所有等式的集合稱為一個等式理論（通俗的解釋）代數(shù)等式理論的定理證明判斷等式 M

12、= N [?]是否在某個代數(shù)等式理論中常用證明方法把M和N分別化簡, 若它們的最簡形式一樣則相等分別證明M和N都等于L證明M?N等于0還有其他方法,12,基 本 知 識,哪種證明方法最適合于計算機(jī)自動證明？把M和N分別化簡, 若它們的最簡形式一樣則相等 若基于等式E，通過等式證明，把M和N化簡到最簡形式，則這種方式相對簡單，便于自動證明 并且采用適合于計算機(jī)使用的單向重寫規(guī)則分別證明M和N都等于L

13、 自動選擇L是非常困難的證明M?N等于0 不適用于非數(shù)值類型的項，例如先前給出的atom類型的表,13,項 重 寫 系 統(tǒng),自動證明要解決的問題項集T 上等式集E中的等式要定向為單向項重寫規(guī)則, 構(gòu)成重寫規(guī)則集R, 以方便計算機(jī)對項化簡若E是：x + 0 = x，x + S(y) = S(x + y) x ? 0 = 0，x ? S(y) = x ? y + x定向成如下的項重寫系統(tǒng)Rx +

14、0 ? x，x + S(y) ? S(x + y)x ? 0 ? 0，x ? S(y) ? x ? y + x記號M ? N：用一條規(guī)則可將項M歸約成N 若規(guī)則L?R?R，含z一次出現(xiàn)的項T，以及使得[SL/z]T?T的代換S，則[SL/z]T ? [SR/z]T,“?”既用于規(guī)則，也用于項的歸約,14,項 重 寫 系 統(tǒng),自動證明要解決的問題項集T 上等式集E中的等式要定向為單向項重寫規(guī)則, 構(gòu)成重寫規(guī)則集R, 以

15、方便計算機(jī)對項化簡若E是：x + 0 = x，x + S(y) = S(x + y) x ? 0 = 0，x ? S(y) = x ? y + x定向成如下的項重寫系統(tǒng)Rx + 0 ? x，x + S(y) ? S(x + y)x ? 0 ? 0，x ? S(y) ? x ? y + x記號M ? N：用一條規(guī)則可將項M歸約成N例：x + S(S(y)),“?”既用于規(guī)則，也用于項的歸約,15,項

16、 重 寫 系 統(tǒng),自動證明要解決的問題項集T 上等式集E中的等式要定向為單向項重寫規(guī)則, 構(gòu)成重寫規(guī)則集R, 以方便計算機(jī)對項化簡若E是：x + 0 = x，x + S(y) = S(x + y) x ? 0 = 0，x ? S(y) = x ? y + x定向成如下的項重寫系統(tǒng)Rx + 0 ? x，x + S(y) ? S(x + y)x ? 0 ? 0，x ? S(y) ? x ? y + x

17、記號M ? N：用一條規(guī)則可將項M歸約成N例：x + S(S(y)) ? S(x + S(y)) [S(x + S(y))/z]z ? [S(S(x + y))/z]z,16,代換S：x?x y?S(y),項 重 寫 系 統(tǒng),自動證明要解決的問題項集T 上等式集E中的等式要定向為單向項重寫規(guī)則, 構(gòu)成重寫規(guī)則集R, 以方便計算機(jī)對項化簡若E是：x + 0 = x，x + S(y) = S(x +

18、 y) x ? 0 = 0，x ? S(y) = x ? y + x定向成如下的項重寫系統(tǒng)Rx + 0 ? x，x + S(y) ? S(x + y)x ? 0 ? 0，x ? S(y) ? x ? y + x記號M ? N：用一條規(guī)則可將項M歸約成N例：x + S(S(y)) ? S(x + S(y)) ? S(S(x + y)) 子項能與第2條規(guī)則的左部匹配,17,項 重 寫 系

19、統(tǒng),自動證明要解決的問題問題1：如何從E得到R，保證項的化簡能終止例：若有規(guī)則 x + y = y + x，不管怎么定向都有 a + b ? b + a ? a + b ? …問題2：如何從E得到R，保證對項采用不同化簡策略所得最簡項是唯一的（合流性） E：? = S(?), Eq(x, x) = true, Eq(x, S(x)) = falseR：? ? S(?), Eq(x, x) ? true

20、, Eq(x, S(x)) ? false,18,項 重 寫 系 統(tǒng),自動證明要解決的問題問題1：如何從E得到R，保證項的化簡能終止例：若有規(guī)則 x + y = y + x，不管怎么定向都有 a + b ? b + a ? a + b ? …問題2：如何從E得到R，保證對項采用不同化簡策略所得最簡項是唯一的（合流性）R：? ? S(?), Eq(x, x) ? true, Eq(x, S(x)) ? fa

21、lse則有： Eq(?, ?) ? true Eq(?, ?) ? Eq(?, S(?)) ? false問題3：如何從E得到R,使得E和R確定同樣的代數(shù)理論，即在E中能證則在R中也能證（完備性）,19,項 重 寫 系 統(tǒng),問題一：終止性1. 終止性 項集T 上的R不存在無窮歸約序列M0?M1?M2 ?…, 即: 任何項都能歸約到范式(不能再歸約的項)2. 有時很難對等式定向，以得到終止的重寫系統(tǒng)

22、例如：對由三角函數(shù)公式構(gòu)成的等式系統(tǒng) 和角公式: sin(?+?) = sin? cos? + cos? sin?, … 差角公式: sin(? ? ?) = sin? cos? ? cos? sin?, … 積化和差: sin? cos? = (sin(?+?)+sin(???))/2, … 和差化積: sin?+sin? = 2sin((?+?)/2)cos((???)/2), … … …,20,項 重 寫 系

23、 統(tǒng),問題一：終止性3. 定義：良基關(guān)系（良基：well-founded）集合A上的二元關(guān)系?是良基的，若不存在A上元素的無窮遞減序列a0 ? a1 ? a2 ?…（a ? b iff b ? a）例：自然數(shù)上的‘<’關(guān)系是良基的，但‘?’關(guān)系不是4. 若項集T 和良基集A有映射f :T ?A, 滿足T 上任意歸約序列 M0? M1? M2? … ? Mn f f

24、 f fA上存在遞減序列 a0 ? a1 ? a2 ? … ? an 則T 上不存在無窮的歸約序列,21,項 重 寫 系 統(tǒng),問題一：終止性5. 定理令R是項集T 上的一個重寫系統(tǒng)，若能找到有良基關(guān)系的集合A和映射f :T ?A，使得對R中每條規(guī)則L? R都有f (L) ? f (R) ,那么R是終止的注：由此定理，判斷R的終止性成為可能6. f

25、的選擇基于項的語法特點(diǎn)，或者給項指派一種語義例1（基于語法特點(diǎn)：根據(jù)兩邊項語法上的繁簡） first(cons(x, l)) ? xrest(cons(x, l)) ? l,22,項 重 寫 系 統(tǒng),問題一：終止性例2（邏輯運(yùn)算系統(tǒng)）?? x ? x ?：就是C中的&& ? (x ? y) ? (?x ? ?y) ?：就是C中的 || ? (x ? y) ? (?x

26、 ? ?y) ?：就是C中的！x ? (y ? z) ? (x ? y) ? (x ? z)(y ? z) ? x ? (y ? x) ? (z ? x),23,項 重 寫 系 統(tǒng),問題一：終止性例2（邏輯運(yùn)算系統(tǒng)，給項指派一種語義）?? x ? x A ? N ? ?0, 1? ? (x ? y) ? (?x ? ?y) ?A(x, y) = x + y + 1? (x ? y) ?

27、(?x ? ?y) ?A(x, y) = x ? yx ? (y ? z) ? (x ? y) ? (x ? z)?A(x) = 2x(y ? z) ? x ? (y ? x) ? (z ? x)語義指派f 應(yīng)用到T 、?、 ?和?的結(jié)果分別是A、 ?A、?A和?A，后三者都是A上的二元或一元函數(shù)對每條規(guī)則L ? R，都有f (L) ? f (R)規(guī)則1：?x >1, 有 > x規(guī)則2：?

28、x, y >1, 有2(x+y+1) = 2x2y2 > 2x2y,24,項 重 寫 系 統(tǒng),問題二：合流性1. 記號 M?N：M經(jīng)若干步(含0步)重寫后得到N N?M：若有M?N M? ? ?N：若存在P，使得M?P且N?P2. 定義 令R是項集T 上的重寫系統(tǒng),若N ? M ? P 蘊(yùn)涵N ? ? ? P，則R是合流的3. 定義 令R是項集T 上的重寫系統(tǒng),若N ? M ? P 蘊(yùn)涵N ? ?

29、? P，則R是局部合流的 局部合流關(guān)系嚴(yán)格弱于合流關(guān)系先考慮局部合流的判定方法，然后再考慮合流的判定方法,25,項 重 寫 系 統(tǒng),插曲在介紹局部合流性之前，先介紹代數(shù)項的樹形表示代數(shù)項cons(first(cons(x, l)), rest(cons(y, l)))的樹形表示倒長的樹：根在上，葉在下每棵子樹代表一個子項，整個樹代表完整的代數(shù)項,26,項 重 寫 系 統(tǒng),局部合流性的判定（問題二的子問題）1. 討論所

30、選用的例子函數(shù)：nil : listcons : atom ? list ? list first : list ? atom，rest : list ? list cond : bool ? list ? list ? list等式： first(cons(x, l)) = x, rest(cons(x, l)) = l, cons(first(l), rest(l)) = l,

31、 … … 下面的討論針對如下兩條重寫規(guī)則：rest(cons(x, l)) ? lcons(first(l?), rest(l?)) ? l?,27,項 重 寫 系 統(tǒng),局部合流性的判定（問題二的子問題） (1) 無重疊的歸約 歸約規(guī)則： rest(cons(x, l)) ? l （規(guī)則L?R） cons(first(l?), rest(l?)) ? l? （規(guī)則

32、L??R?） 待歸約項：cond (B, rest(cons s l), cons(first(l), rest(l)) ) ? 方式1: 原式 ? cond(B, l, cons(first(l), rest(l)) ) ? cond(B, l, l) ? 方式2: 原式 ? cond (B, rest(cons s l), l) ? cond(B,

33、 l, l) 特點(diǎn)：M中無重疊子項的歸約相互不受影響,28,項 重 寫 系 統(tǒng),局部合流性的判定 (1) 無重疊的歸約圖示：L?R 和L??R?是規(guī)則圖中SL和SR分別表示 代換S作用于L的 結(jié)果 S : T ?T代換S的最主要部分是把變量映射到項,29,cond (B, rest(cons s l), cons(first(l), rest(l))),項 重

34、寫 系 統(tǒng),局部合流性的判定（問題二的子問題） (2) 平凡的重疊 歸約規(guī)則：rest(cons(x, l)) ? l（規(guī)則L?R） cons(first(l?), rest(l?)) ? l?（規(guī)則L??R?） 待歸約項： rest(cons(x, cons(first(l), rest(l))) ? 方式1: 原式 ? cons(first(l), rest(l)) ?

35、l ? 方式2: 原式 ? rest(cons(x, l)) ? l,,30,項 重 寫 系 統(tǒng),局部合流性的判定（問題二的子問題） (2) 平凡的重疊 歸約規(guī)則：rest(cons(x, l)) ? l（規(guī)則L?R） cons(first(l?), rest(l?)) ? l?（規(guī)則L??R?） 待歸約項： rest(cons(x, cons(first(l), rest(

36、l))) 特點(diǎn)：SL?是SL的子項，且S把L中的某變量(這里是l)用由SL?構(gòu)成的項代換 不同的第1步歸約不會影響局部合流，但合流所需歸約步數(shù)可能不一樣（取決于R中有幾個l）,,31,項 重 寫 系 統(tǒng),局部合流性的判定 (2) 平凡的重疊 圖示：SL?是SL的子項，且S把L中的某變量x用有SL?構(gòu)成的項代換不同的第1步歸約不會影響局部合流，但合流所需歸約步數(shù)可能不一樣,32,rest(co

37、ns(x, cons(first(l), rest(l))),項 重 寫 系 統(tǒng),局部合流性的判定（問題二的子問題）(3) 非平凡的重疊 歸約規(guī)則：rest(cons(x, l)) ? l（規(guī)則L?R） cons(first(l?), rest(l?))? l?（規(guī)則L??R?） 待歸約項：rest(cons(first(l), rest(l))) ? 方式1: 原

38、式 ? rest(l)（用規(guī)則L?R） ? 方式2: 原式 ? rest(l)（用規(guī)則L??R?） 該例比較特殊，都一步歸約就到范式,,33,項 重 寫 系 統(tǒng),局部合流性的判定（問題二的子問題）(3) 非平凡的重疊 歸約規(guī)則：rest(cons(x, l)) ? l（規(guī)則L?R） cons(first(l?), rest(l?))? l?（規(guī)則L??R?） 待歸約項：

39、rest(cons(first(l), rest(l))) 特點(diǎn)：SL?在SL的非變量位置L?R 或L??R?的使用都可能使對方在原定位置 不能使用，故不能保證局部合流,,34,項 重 寫 系 統(tǒng),局部合流性的判定(3) 非平凡的重疊 圖示：SL?在SL的非變量位置L?R或L??R?的使用都可能使對方在原定位置不能使用，故不能保證局部合流,35,rest(cons(first(l), res

40、t(l))),項 重 寫 系 統(tǒng),局部合流性的判定若所有含非平凡重疊的項都能局部合流, 則R也能把對所有含非平凡重疊的項的檢查縮小為對有限的重寫規(guī)則集的檢查 若由R的重寫規(guī)則確定的所有關(guān)鍵對(critical pair)都能歸約到同一個項，則所有項的非平凡重疊都能局部合流（課堂上不介紹）例：重寫規(guī)則rest(cons(x, l)) ? l，和 cons(first(l?), rest(l?)) ? l

41、?會形成兩個關(guān)鍵對,36,項 重 寫 系 統(tǒng),第1個關(guān)鍵對：（課堂上不介紹）選適當(dāng)?shù)拇鷵Q，使得兩規(guī)則代換后綠色部分一樣cons(first(l?), rest(l?)) ? l? rest(cons(x, l)) ? l第1條規(guī)則中的l?用cons(x, l)代換后, 其左部是項：cons(first(cons(x, l)), (rest(cons(x, l)))用這兩條規(guī)則化簡上述

42、項可得第1個關(guān)鍵對：? cons(x, l), cons(first(cons(x, l)), l) ?歸約關(guān)鍵對：cons(x, l)已經(jīng)是范式 cons(first(cons(x, l)), l) ? cons(x, l)第1個關(guān)鍵對能歸約到同一個項,37,項 重 寫 系 統(tǒng),第2個關(guān)鍵對：（課堂上不介紹）選適當(dāng)?shù)拇鷵Q，使得兩規(guī)則代換后綠色部分一樣 cons(first(l?), rest

43、(l?)) ? l?rest(cons(x, l)) ? l第2條規(guī)則中的x和l分別代換成first(l?)和rest(l?)后,其左部是項：rest(cons(first(l?), rest(l?)))用這兩條規(guī)則化簡上述項可得第2個關(guān)鍵對：? rest(l?), rest(l?) ?顯然，第2個關(guān)鍵對也能歸約到同一個項,38,項 重 寫 系 統(tǒng),局部合流性的判定定理 一個重寫系統(tǒng)R是局部合流的，當(dāng)且僅當(dāng)

44、對每個關(guān)鍵對?M, N?有M ? ? ? N如果一個有限的重寫系統(tǒng)R是終止的，那么該定理就給出一個算法，可用于判定R是否局部合流,39,項 重 寫 系 統(tǒng),局部合流、終止和合流之間的聯(lián)系定理 令R是終止的重寫系統(tǒng)，那么R是合流的當(dāng)且僅當(dāng)它是局部合流的合流蘊(yùn)含局部合流（這是顯然的）反方向蘊(yùn)含的證明需要使用良基歸納法,40,良 基 歸 納 法,良基歸納法用一個簡單例子說明它比自然數(shù)歸納法更一般證明：對任何自然數(shù)的有限集合，每

45、次刪除一個元 素，最終會到達(dá)空集 1. 若忽略集合中元素的個性，只關(guān)心集合中元素的個數(shù)，則可以用自然數(shù)歸納法 2. 若關(guān)注元素個性（雖無必要）? ：集合之間的歸約規(guī)則: {x1, …, xn}?{x2, …, xn}其中x1是左邊集合的任意元素 3.良基關(guān)系：A ? B則A ? B,41,良 基 歸 納 法,良基歸納法需要證明：任何自然數(shù)的有限集合可歸約到空集1. 對所有的歸約路徑進(jìn)

46、行歸納2. 良基歸納證明歸納基礎(chǔ)：?經(jīng)0步歸約到?歸納假設(shè)：對所有的s ? s1, s ? s2,…, s ? sn, s1, s2, …, sn都能歸約到?歸納證明：證明s能歸約到?,42,良 基 歸 納 法,良基歸納法（課堂上不介紹）令?是集合A上的一個良基關(guān)系，令P是A上的某個性質(zhì)。若每當(dāng)所有的P(b) (b ? a)為真則P(a)為真(即?a.(?b.(b ? a ? P(b)) ? P(a)) )，

47、那么，對所有的a?A，P(a)為真證明步驟：歸納基礎(chǔ): 對任意不存在b使得b ? a的a，證明P(a) 在不存在b使得b ? a的情況下， ?b.(b ? a ? P(b)) ? P(a)等價于 true ? P(a)等價于 P(a),43,良 基 歸 納 法,良基歸納法（課堂上不介紹）令?是集合A上的一個良基關(guān)系，令P是A上的某個性質(zhì)。若每當(dāng)所有的P(b) (b

48、 ? a)為真則P(a)為真(即?a.(?b.(b ? a ? P(b)) ? P(a)) )，那么，對所有的a?A，P(a)為真證明步驟：歸納基礎(chǔ): 對任意不存在b使得b ? a的a，證明P(a)歸納步驟：對任意存在b使得b ? a的a，?b.(b ? a ? P(b)) ? P(a)在此得出歸納假設(shè)： 假定對所有b ? a的b，P(b)為真，然后證明：歸納證明：證明P(a)為真,44,良 基 歸 納

49、法,用良基歸納法證明合流性證明：若有M? N和 M? P，則N? ? ?P若M?N, 則規(guī)定N?M。因系統(tǒng)終止, 故?是良基的歸納基礎(chǔ)： 若不存在N使得N ? M，即M是范式，顯然M具有要證明的性質(zhì) 因為M只能0步歸約到M本身，圖上的N和P都只能是M,45,良 基 歸 納 法,用良基歸納法證明合流性證明：若有M? N和 M? P，則N? ? ?P若M?N, 則規(guī)定N?M。因系統(tǒng)終止, 故?是良

50、基的歸納步驟：假定M? N1? N并且M? P1? P(1) 根據(jù)局部合流性，存在Q，使得N1? Q ?P1,46,良 基 歸 納 法,用良基歸納法證明合流性證明：若有M? N和 M? P，則N? ? ?P若M?N, 則規(guī)定N?M。因系統(tǒng)終止, 故?是良基的歸納步驟： 假定M? N1? N并且M? P1? P(1) 根據(jù)局部合流性，存在Q，使得N1? Q ?P1,47,良 基 歸 納 法,用良基歸

51、納法證明合流性證明：若有M? N和 M? P，則N? ? ?P若M?N, 則規(guī)定N?M。因系統(tǒng)終止, 故?是良基的歸納步驟： 假定M? N1? N并且M? P1? P(2) 由歸納假設(shè)，存在R， 使得N? R ?Q,48,良 基 歸 納 法,用良基歸納法證明合流性證明：若有M? N和 M? P，則N? ? ?P若M?N, 則規(guī)定N?M。因系統(tǒng)終止, 故?是良基的歸納步驟： 假定M? N1? N并且

52、M? P1? P(2) 由歸納假設(shè)，存在R， 使得N? R ?Q,M,49,良 基 歸 納 法,用良基歸納法證明合流性證明：若有M? N和 M? P，則N? ? ?P若M?N, 則規(guī)定N?M。因系統(tǒng)終止, 故?是良基的歸納步驟： 假定M? N1? N并且M? P1? P(3) 再由歸納假設(shè)，存在S， 使得R ? S ?P,M,50,良 基 歸 納 法,用良基歸納法證明合流性證明：若有M? N和 M?

53、P，則N? ? ?P若M?N, 則規(guī)定N?M。因系統(tǒng)終止, 故?是良基的歸納步驟： 假定M? N1? N并且M? P1? P(3) 再由歸納假設(shè)，存在S， 使得R ? S ?P(4) N? ? ?P得證,51,Knuth-Bendix完備化過程,問題三：完備性回顧最適合于計算機(jī)自動證明代數(shù)等式M=N的方式： 把M和N分別化簡, 若它們的最簡形式一樣則相等由定向代數(shù)等式系統(tǒng)E來得到等價的重寫系統(tǒng)R，需解

54、決三個問題：終止性、合流性和完備性完備性：從E可得到R，E和R確定同樣的代數(shù)理論概要介紹Knuth-Bendix完備化過程 給出一個完備化過程不終止的例子。由此可知，并非對任何E都可以得到與之有同樣代數(shù)理論的R,52,Knuth-Bendix完備化過程,Knuth-Bendix完備化過程的目的完備化過程的目的為一個代數(shù)等式系統(tǒng)E，構(gòu)造一個確定同樣代數(shù)理論的終止且合流的重寫系統(tǒng)R,53,Knuth-Bendix完備化過程,Knu

55、th-Bendix完備化過程簡介1. 把E定向成一個終止的重寫系統(tǒng)R（若定向失敗，則完備化過程失?。?. 檢查R的局部合流性并進(jìn)行完備化for(R的每個關(guān)鍵對?M, N?) { if (不具備M? ? ?N){ 把M?N或N?M加入R（原因稍后解釋） （若定向失敗，則完備化過程失?。?} } (過程可能因R不斷地被加入規(guī)則而不終止)3. 最終的R為所求,54,K

56、nuth-Bendix完備化過程,例：完備化過程不終止作為輸入的等式系統(tǒng)E如下f(x) ? f(y) = f(x + y)(x + y) + z = x + (y + z)1. 先定向成一個終止的重寫系統(tǒng)R f(x) ? f(y) ? f(x + y) (x + y) + z ? x + (y + z)2. 檢查局部合流性并進(jìn)行完備化,55,Knuth-Bendix完備化過程,例：完備化過程不終止作為輸入的等式系

57、統(tǒng)E如下f(x) ? f(y) = f(x + y)(x + y) + z = x + (y + z)1. 先定向成一個終止的重寫系統(tǒng)R f(x) ? f(y) ? f(x + y) (x + y) + z ? x + (y + z)2. 檢查局部合流性并進(jìn)行完備化(1) 把兩條規(guī)則左部的綠色部分進(jìn)行合一，產(chǎn)生一個臨界對? f(x + y) + z, f(x) + (f(y) + z) ?臨界對的兩個項都

58、已最簡，這個臨界對不能合流,因第2條規(guī)則左部的合一結(jié)果： (f(x) ? f(y)) + z,56,Knuth-Bendix完備化過程,例：完備化過程不終止作為輸入的等式系統(tǒng)E如下f(x) ? f(y) = f(x + y)(x + y) + z = x + (y + z)1. 先定向成一個終止的重寫系統(tǒng)R f(x) ? f(y) ? f(x + y) (x + y) + z ? x + (y + z)2. 檢查局

59、部合流性并進(jìn)行完備化(1) 把兩條規(guī)則左部的綠色部分進(jìn)行合一，產(chǎn)生一個臨界對? f(x + y) + z, f(x) + (f(y) + z) ?(2) 增加重寫規(guī)則f(x + y) + z ? f(x) + (f(y) + z),因第2條規(guī)則左部的合一結(jié)果： (f(x) ? f(y)) + z,57,Knuth-Bendix完備化過程,例：完備化過程不終止解釋：增加規(guī)則f(x + y) + z ? f(x) + (f(y

60、) + z)的原因在E中可證f(x + y) + z和f(x) + (f(y) + z)相等等式：f(x) ? f(y) = f(x + y)和(x + y) + z = x + (y + z) 證明：f(x + y) + z = f(x) ? f(y) + z = f(x) + (f(y) + z)在未加上述重寫規(guī)則R中證明不了, 即R不完備： 在R中能證的等式在E中能證，但存在E中能證而在R中不能證的等式向R中

61、加規(guī)則是為了完備性,58,Knuth-Bendix完備化過程,例（續(xù)）1. 先定向成一個終止的重寫系統(tǒng)R f(x) ? f(y) ? f(x + y) (x + y) + z ? x + (y + z)2. 檢查局部合流性并進(jìn)行完備化(1) 產(chǎn)生一個臨界對? f(x + y) + z, f(x) + (f(y) + z) ? (2) 增加重寫規(guī)則f(x + y) + z ? f(x) + (f(y) + z)

62、(3) R擴(kuò)大為： f(x) ? f(y) ? f (x + y) (x + y) + z ? x + (y + z) f(x + y) + z ? f(x) + (f(y) + z),59,Knuth-Bendix完備化過程,例（續(xù)）1. 先定向成一個終止的重寫系統(tǒng)R f(x) ? f(y) ? f(x + y) (x + y) + z ? x + (y + z)2. 檢查局部合流性并進(jìn)行完

63、備化(1) 產(chǎn)生一個臨界對? f(x + y) + z, f(x) + (f(y) + z) ? (2) 增加重寫規(guī)則f(x + y) + z ? f(x) + (f(y) + z)(3) R擴(kuò)大為： f(x) ? f(y) ? f (x + y) (x + y) + z ? x + (y + z) f(x + y) + z ? f(x) + (f(y) + z)兩條規(guī)則中的綠色部分也

64、可以合一,60,Knuth-Bendix完備化過程,例（續(xù)）1. 先定向成一個終止的重寫系統(tǒng)R f(x) ? f(y) ? f(x + y) (x + y) + z ? x + (y + z)2. 檢查局部合流性并進(jìn)行完備化(1) 產(chǎn)生一個臨界對? f(x + y) + z, f(x) + (f(y) + z) ? (2) 增加重寫規(guī)則f(x + y) + z ? f(x) + (f(y) + z)(3) R

65、擴(kuò)大為： f(x) ? f(y) ? f (x + y) (x + y) + z ? x + (y + z) f(x + y) + z ? f(x) + (f(y) + z)將產(chǎn)生無數(shù)規(guī)則: f n(x + y) + z ? f n(x) + (f n(y) + z),完備化過程因不斷產(chǎn)生新的規(guī)則而不終止,61,自 動 定 理 證 明,不同邏輯的自動定理證明方法可能不一樣本講座介紹代數(shù)等式理論的自

66、動定理證明，并未徹底解決其他還有：命題邏輯的自動定理證明幾何定理的自動證明… …多種理論組合的自動定理證明其中有些已徹底解決，有些在一定約束下可以解決,62,構(gòu)造性證明與傳統(tǒng)證明對比,傳統(tǒng)證明的一個例子證明根據(jù) 是有理數(shù)或無理數(shù)來討論,若 是有理數(shù)，則取x = 3若是無理數(shù)，則取x =這種非構(gòu)造性證明不太可能由計算機(jī)自動得到,63,小 結(jié),本講座小結(jié)

67、以代數(shù)等式理論中的定理證明為例，介紹怎樣從熟知的等式演算方法，構(gòu)造自動定理證明系統(tǒng)不同邏輯的自動定理證明方法不同自動定理證明的應(yīng)用集成電路設(shè)計程序驗證程序分析相關(guān)課程數(shù)理邏輯、人工智能,64,小 結(jié),工具交互式定理證明輔助工具Coqhttp://coq.inria.fr/，獲ACM 2013年度軟件系統(tǒng)獎自動定理證明器Z31. http://research.microsoft.com/en-us/um/

68、 redmond/projects/z3/old/index.html2. http://z3.codeplex.com/，獲ACM 2015年度編程語言軟件獎,65,小 結(jié),參考文獻(xiàn)Daniel Kroening and Ofer Strichman，Decision Procedures: An Algorithmic Point of View (Texts in Theoretical Computer Sci