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

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

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

3、行問(wèn)題求解、系統(tǒng)設(shè)計(jì)、以及人類(lèi)行為理解等涵蓋計(jì)算機(jī)科學(xué)之廣度的一系列思維活動(dòng),3,講 座 提 綱,基本知識(shí)代數(shù)項(xiàng)、代數(shù)等式、演繹推理規(guī)則、代數(shù)等式理論、等式定理證明方法項(xiàng)重寫(xiě)系統(tǒng)終止性、良基關(guān)系、合流性、局部合流性、關(guān)鍵對(duì)良基歸納法僅舉例說(shuō)明Knuth-Bendix完備化過(guò)程也僅舉例說(shuō)明,4,基 本 知 識(shí),代數(shù)項(xiàng)和代數(shù)等式（僅涉及一個(gè)類(lèi)型）代數(shù)項(xiàng)例：自然數(shù)類(lèi)型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ù)項(xiàng)代數(shù)等式例： x + 0 = x，x + S(y) = S(x + y) x + y = z + 5,5,基

5、 本 知 識(shí),代數(shù)項(xiàng)和代數(shù)等式（涉及多個(gè)類(lèi)型）例：定義有限表：同類(lèi)數(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ù)涉及兩個(gè)類(lèi)型 ? 序列中元素的類(lèi)型 — 數(shù)值或非數(shù)值類(lèi)型 ? 這些序列所屬的類(lèi)

6、型，稱(chēng)為表（list）類(lèi)型 —非數(shù)值類(lèi)型中學(xué)所學(xué)的代數(shù)概念在此已經(jīng)擴(kuò)展,6,基 本 知 識(shí),代數(shù)項(xiàng)和代數(shù)等式（涉及多個(gè)類(lèi)型）代數(shù)項(xiàng)（表類(lèi)型list ，表元類(lèi)型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ù)項(xiàng)。用T 表示項(xiàng)集代數(shù)等式(方括號(hào)列出等式中出現(xiàn)的變量及類(lèi)型) first(cons(x, l)) = x [x : atom,

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

9、規(guī)則：加變量規(guī)則：等價(jià)代換規(guī)則：,基 本 知 識(shí),x不在?中,P , Q 是類(lèi)型s的項(xiàng),9,等式推理的例子等價(jià)代換規(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))使用等價(jià)代換規(guī)則得到第一個(gè)等式 S(x +

10、 S(y)) 根據(jù)S(z) = S(z)，x + S(y) = S(x + y)= S(S(x + y)) 使用等價(jià)代換規(guī)則得到第二個(gè)等式x + S(S(y)) = S(S(x + y)) 根據(jù)傳遞規(guī)則和上面兩等式,基 本 知 識(shí),10,等式推理的例子等價(jià)代換規(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í)慣見(jiàn)左邊= S(S(x + y)) 它是基于剛才所介紹的演繹推理的若希望計(jì)算機(jī)來(lái)自動(dòng)推理，嚴(yán)格的推理規(guī)則是必須提供的,基 本 知 識(shí),11,基 本 知 識(shí),代數(shù)等式理論（algebraic equation theory）在項(xiàng)集T 上從一組等式E（公理）能推出的所有等式的集合稱(chēng)為一個(gè)等式理論（通俗的解釋?zhuān)┐鷶?shù)等式理論的定理證明判斷等式 M

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

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

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

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

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

17、記號(hào)M ? N：用一條規(guī)則可將項(xiàng)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),項(xiàng) 重 寫(xiě) 系 統(tǒng),自動(dòng)證明要解決的問(wèn)題項(xiàng)集T 上等式集E中的等式要定向?yàn)閱蜗蝽?xiàng)重寫(xiě)規(guī)則, 構(gòu)成重寫(xiě)規(guī)則集R, 以方便計(jì)算機(jī)對(duì)項(xiàng)化簡(jiǎn)若E是：x + 0 = x，x + S(y) = S(x +

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

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

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

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

22、例如：對(duì)由三角函數(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,項(xiàng) 重 寫(xiě) 系

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

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

25、的選擇基于項(xiàng)的語(yǔ)法特點(diǎn)，或者給項(xiàng)指派一種語(yǔ)義例1（基于語(yǔ)法特點(diǎn)：根據(jù)兩邊項(xiàng)語(yǔ)法上的繁簡(jiǎn)） first(cons(x, l)) ? xrest(cons(x, l)) ? l,22,項(xiàng) 重 寫(xiě) 系 統(tǒng),問(wèn)題一：終止性例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,項(xiàng) 重 寫(xiě) 系 統(tǒng),問(wèn)題一：終止性例2（邏輯運(yùn)算系統(tǒng)，給項(xiàng)指派一種語(yǔ)義）?? 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)語(yǔ)義指派f 應(yīng)用到T 、?、 ?和?的結(jié)果分別是A、 ?A、?A和?A，后三者都是A上的二元或一元函數(shù)對(duì)每條規(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,項(xiàng) 重 寫(xiě) 系 統(tǒng),問(wèn)題二：合流性1. 記號(hào) M?N：M經(jīng)若干步(含0步)重寫(xiě)后得到N N?M：若有M?N M? ? ?N：若存在P，使得M?P且N?P2. 定義 令R是項(xiàng)集T 上的重寫(xiě)系統(tǒng),若N ? M ? P 蘊(yùn)涵N ? ? ? P，則R是合流的3. 定義 令R是項(xiàng)集T 上的重寫(xiě)系統(tǒng),若N ? M ? P 蘊(yùn)涵N ? ?

29、? P，則R是局部合流的 局部合流關(guān)系嚴(yán)格弱于合流關(guān)系先考慮局部合流的判定方法，然后再考慮合流的判定方法,25,項(xiàng) 重 寫(xiě) 系 統(tǒng),插曲在介紹局部合流性之前，先介紹代數(shù)項(xiàng)的樹(shù)形表示代數(shù)項(xiàng)cons(first(cons(x, l)), rest(cons(y, l)))的樹(shù)形表示倒長(zhǎng)的樹(shù)：根在上，葉在下每棵子樹(shù)代表一個(gè)子項(xiàng)，整個(gè)樹(shù)代表完整的代數(shù)項(xiàng),26,項(xiàng) 重 寫(xiě) 系 統(tǒng),局部合流性的判定（問(wèn)題二的子問(wèn)題）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、 … … 下面的討論針對(duì)如下兩條重寫(xiě)規(guī)則：rest(cons(x, l)) ? lcons(first(l?), rest(l?)) ? l?,27,項(xiàng) 重 寫(xiě) 系 統(tǒng),局部合流性的判定（問(wèn)題二的子問(wèn)題） (1) 無(wú)重疊的歸約 歸約規(guī)則： rest(cons(x, l)) ? l （規(guī)則L?R） cons(first(l?), rest(l?)) ? l? （規(guī)則

32、L??R?） 待歸約項(xiàng)：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中無(wú)重疊子項(xiàng)的歸約相互不受影響,28,項(xiàng) 重 寫(xiě) 系 統(tǒng),局部合流性的判定 (1) 無(wú)重疊的歸約圖示：L?R 和L??R?是規(guī)則圖中SL和SR分別表示 代換S作用于L的 結(jié)果 S : T ?T代換S的最主要部分是把變量映射到項(xiàng),29,cond (B, rest(cons s l), cons(first(l), rest(l))),項(xiàng) 重

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

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

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

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

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

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

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

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

42、項(xiàng)可得第1個(gè)關(guān)鍵對(duì)：? cons(x, l), cons(first(cons(x, l)), l) ?歸約關(guān)鍵對(duì)：cons(x, l)已經(jīng)是范式 cons(first(cons(x, l)), l) ? cons(x, l)第1個(gè)關(guān)鍵對(duì)能歸約到同一個(gè)項(xiàng),37,項(xiàng) 重 寫(xiě) 系 統(tǒng),第2個(gè)關(guān)鍵對(duì)：（課堂上不介紹）選適當(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?)后,其左部是項(xiàng)：rest(cons(first(l?), rest(l?)))用這兩條規(guī)則化簡(jiǎn)上述項(xiàng)可得第2個(gè)關(guān)鍵對(duì)：? rest(l?), rest(l?) ?顯然，第2個(gè)關(guān)鍵對(duì)也能歸約到同一個(gè)項(xiàng),38,項(xiàng) 重 寫(xiě) 系 統(tǒng),局部合流性的判定定理 一個(gè)重寫(xiě)系統(tǒng)R是局部合流的，當(dāng)且僅當(dāng)

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

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

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

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

48、 ? a)為真則P(a)為真(即?a.(?b.(b ? a ? P(b)) ? P(a)) )，那么，對(duì)所有的a?A，P(a)為真證明步驟：歸納基礎(chǔ): 對(duì)任意不存在b使得b ? a的a，證明P(a)歸納步驟：對(duì)任意存在b使得b ? a的a，?b.(b ? a ? P(b)) ? P(a)在此得出歸納假設(shè)： 假定對(duì)所有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ì) 因?yàn)镸只能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完備化過(guò)程,問(wèn)題三：完備性回顧最適合于計(jì)算機(jī)自動(dòng)證明代數(shù)等式M=N的方式： 把M和N分別化簡(jiǎn), 若它們的最簡(jiǎn)形式一樣則相等由定向代數(shù)等式系統(tǒng)E來(lái)得到等價(jià)的重寫(xiě)系統(tǒng)R，需解

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

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

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

57、統(tǒng)E如下f(x) ? f(y) = f(x + y)(x + y) + z = x + (y + z)1. 先定向成一個(gè)終止的重寫(xiě)系統(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)生一個(gè)臨界對(duì)? f(x + y) + z, f(x) + (f(y) + z) ?臨界對(duì)的兩個(gè)項(xiàng)都

58、已最簡(jiǎn)，這個(gè)臨界對(duì)不能合流,因第2條規(guī)則左部的合一結(jié)果： (f(x) ? f(y)) + z,56,Knuth-Bendix完備化過(guò)程,例：完備化過(guò)程不終止作為輸入的等式系統(tǒng)E如下f(x) ? f(y) = f(x + y)(x + y) + z = x + (y + z)1. 先定向成一個(gè)終止的重寫(xiě)系統(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)生一個(gè)臨界對(duì)? f(x + y) + z, f(x) + (f(y) + z) ?(2) 增加重寫(xiě)規(guī)則f(x + y) + z ? f(x) + (f(y) + z),因第2條規(guī)則左部的合一結(jié)果： (f(x) ? f(y)) + z,57,Knuth-Bendix完備化過(guò)程,例：完備化過(guò)程不終止解釋?zhuān)涸黾右?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)在未加上述重寫(xiě)規(guī)則R中證明不了, 即R不完備： 在R中能證的等式在E中能證，但存在E中能證而在R中不能證的等式向R中

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

63、備化(1) 產(chǎn)生一個(gè)臨界對(duì)? f(x + y) + z, f(x) + (f(y) + z) ? (2) 增加重寫(xiě)規(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完備化過(guò)程,例（續(xù)）1. 先定向成一個(gè)終止的重寫(xiě)系統(tǒng)R f(x) ? f(y) ? f(x + y) (x + y) + z ? x + (y + z)2. 檢查局部合流性并進(jìn)行完備化(1) 產(chǎn)生一個(gè)臨界對(duì)? f(x + y) + z, f(x) + (f(y) + z) ? (2) 增加重寫(xiě)規(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)生無(wú)數(shù)規(guī)則: f n(x + y) + z ? f n(x) + (f n(y) + z),完備化過(guò)程因不斷產(chǎn)生新的規(guī)則而不終止,61,自 動(dòng) 定 理 證 明,不同邏輯的自動(dòng)定理證明方法可能不一樣本講座介紹代數(shù)等式理論的自

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

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

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