代數(shù)等式理論的自動(dòng)定理證明計(jì)算機(jī)科學(xué)導(dǎo)論第一講-資料下載頁(yè)
2025-07-18 08:22本頁(yè)面
【正文】 KnuthBendix完備化過(guò)程的目的 完備化過(guò)程的目的 – 為一個(gè)代數(shù)等式系統(tǒng) E， 構(gòu)造一個(gè)確定同樣代數(shù)理論的終止且合流的重寫系統(tǒng) R 53 KnuthBendix完備化過(guò)程 ? KnuthBendix完備化過(guò)程簡(jiǎn)介 1. 把 E定向成一個(gè)終止的重寫系統(tǒng) R （ 若定向失敗 ， 則完備化過(guò)程失敗 ） 2. 檢查 R的局部合流性并進(jìn)行完備化 for(R的每個(gè)關(guān)鍵對(duì) ?M, N?) { if (不具備 M? ? ?N){ 把 M?N或 N?M加入 R（ 原因稍后解釋 ） （ 若定向失敗 ， 則完備化過(guò)程失敗 ） } } (過(guò)程可能因 R不斷地被加入規(guī)則而不終止 ) 3. 最終的 R為所求 54 KnuthBendix完備化過(guò)程 ? 例：完備化過(guò)程不終止 作為輸入的等式系統(tǒng) E如下 f(x) ? f(y) = f(x + y) (x + y) + z = x + (y + z) 1. 先定向成一個(gè)終止的重寫系統(tǒng) R f(x) ? f(y) ? f(x + y) (x + y) + z ? x + (y + z) 2. 檢查局部合流性并進(jìn)行完備化 55 KnuthBendix完備化過(guò)程 ? 例：完備化過(guò)程不終止 作為輸入的等式系統(tǒng) E如下 f(x) ? f(y) = f(x + y) (x + y) + z = x + (y + z) 1. 先定向成一個(gè)終止的重寫系統(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)都已最簡(jiǎn) ， 這個(gè)臨界對(duì)不能合流 因第 2條規(guī)則左部的合一結(jié)果： (f(x) ? f(y)) + z 56 KnuthBendix完備化過(guò)程 ? 例：完備化過(guò)程不終止 作為輸入的等式系統(tǒng) E如下 f(x) ? f(y) = f(x + y) (x + y) + z = x + (y + z) 1. 先定向成一個(gè)終止的重寫系統(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) ? (2) 增加 重寫規(guī)則 f(x + y) + z ? f(x) + (f(y) + z) 因第 2條規(guī)則左部的合一結(jié)果： (f(x) ? f(y)) + z 57 KnuthBendix完備化過(guò)程 ? 例：完備化過(guò)程不終止 解釋：增加規(guī)則 f(x + y) + z ? f(x) + (f(y) + 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中加規(guī)則是為了完備性 58 KnuthBendix完備化過(guò)程 ? 例 （ 續(xù) ） 1. 先定向成一個(gè)終止的重寫系統(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) 增加重寫規(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) 59 KnuthBendix完備化過(guò)程 ? 例 （ 續(xù) ） 1. 先定向成一個(gè)終止的重寫系統(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) 增加重寫規(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ī)則中的綠色部分也可以合一 60 KnuthBendix完備化過(guò)程 ? 例 （ 續(xù) ） 1. 先定向成一個(gè)終止的重寫系統(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) 增加重寫規(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) 將產(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ù)等式理論的自動(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é) – 以代數(shù)等式理論中的定理證明為例，介紹怎樣從熟知的等式演算方法 ， 構(gòu)造自動(dòng)定理證明 系統(tǒng) – 不同邏輯的自動(dòng)定理證明方法不同 ? 自動(dòng)定理證明的應(yīng)用 – 集成電路設(shè)計(jì) – 程序驗(yàn)證 – 程序分析 ? 相關(guān)課程 – 數(shù)理邏輯 、 人工智能 64 小 結(jié) ? 工具 – 交互式定理證明輔助工具 Coq 獲 ACM 2022年度軟件系統(tǒng)獎(jiǎng) – 自動(dòng)定理證明器 Z3 1. redmond/projects/z3/old/ 2. 獲 ACM 2022年度編程語(yǔ)言軟件獎(jiǎng) 65 小 結(jié) ? 參考文獻(xiàn) – Daniel Kroening and Ofer Strichman， Decision Procedures: An Algorithmic Point of View (Texts in Theoretical Computer Science. An EATCS Series) – 陳意云、張昱，程序設(shè)計(jì)語(yǔ)言理論（第二版），高等教育出版者， 2022年 2月 備注：本次課 的內(nèi)容取自該書前 兩章中有關(guān)代數(shù)數(shù)據(jù)類型的部分 66
試題試卷相關(guān)推薦
鄂ICP備17016276號(hào)-1