畢業(yè)設(shè)計(jì)論文 外文文獻(xiàn)翻譯 自動(dòng)化專業(yè) Automation 中英文對(duì)照

《畢業(yè)設(shè)計(jì)論文 外文文獻(xiàn)翻譯 自動(dòng)化專業(yè) Automation 中英文對(duì)照》由會(huì)員分享，可在線閱讀，更多相關(guān)《畢業(yè)設(shè)計(jì)論文 外文文獻(xiàn)翻譯 自動(dòng)化專業(yè) Automation 中英文對(duì)照（40頁(yè)珍藏版）》請(qǐng)?jiān)谘b配圖網(wǎng)上搜索。

1、編號(hào)： 畢業(yè)設(shè)計(jì)英文翻譯譯文 題 目: Automation 院 〔系〕： 計(jì)算機(jī)系 專 業(yè)： 自動(dòng)化 學(xué)生姓名： 學(xué) 號(hào)： 指導(dǎo)教師： 職 稱： 2005

2、 年 6 月 3日 自動(dòng)化 湯姆里治 2005 年四月 12 日 目 錄 1 介紹 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 2 需求. . . . . . . . . . . . . . . . . . . . . . . . . . . .

3、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 3 目前交互式證明器的自動(dòng)化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4 4 技術(shù). . . . . . . . . . . . . . . . .

4、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 4.1 證明的搜尋. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 邏輯系統(tǒng). . . . . . . . . . . . . . .

5、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 引進(jìn)規(guī)那么. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 4.2 等式. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

6、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 改寫(xiě). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 條件的簡(jiǎn)單化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7、 . . . . . . . . . . . . . . . . . . . . . . . . .9 完成. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 動(dòng)態(tài)的完成. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

8、. . . . . . . . . . .11 方程式的統(tǒng)一. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 5 連接與整合. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12

9、 6 評(píng)估. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 6.1 評(píng)估生產(chǎn)需求. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

10、 . . . . . . . . . . . . . . . . . . . . . . . .13 6.2 完整性. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 6.3 效率. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

11、. . . . . . . . . . . . . . . .14 6.4 實(shí)際應(yīng)用. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 7 替代選擇. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

12、. . 16 8 結(jié)論. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .19 1 介紹 自動(dòng)化可能是成功的機(jī)械化的關(guān)鍵。在一些情形中，機(jī)械化不需要自

13、動(dòng)化就可以實(shí)行。確實(shí)，在高度抽象的數(shù)學(xué)區(qū)域，大局部由使用者拼出的復(fù)雜證明組成的機(jī)械化推論遠(yuǎn)遠(yuǎn)超過(guò)了那些目前能被自動(dòng)化解決的范圍。在這一背景下，如果自動(dòng)化它被全部使用， 將指導(dǎo)在容易的可以解決的被緊緊地限定的次問(wèn)題上。一個(gè)機(jī)械化的典型例子是我們的拉姆齊定理的形式化。另一方面，在推論相對(duì)被限制的地方，自動(dòng)化能富有成效地在確認(rèn)類型的證明中被應(yīng)用，但是絕對(duì)程度的細(xì)節(jié)將使一個(gè)非自動(dòng)化的機(jī)械化不可實(shí)行。 許多人已經(jīng)花費(fèi)了數(shù)年來(lái)開(kāi)展全自動(dòng)系統(tǒng)。比方Vampire [VR] 和otter [McC]全自動(dòng)系統(tǒng)。我們可以和這樣的系統(tǒng)競(jìng)爭(zhēng)的設(shè)想是愚蠢的。它們的執(zhí)行是一種方式，這種方式超過(guò)目前在交互式定理證明器被

14、實(shí)行的系統(tǒng)。這些方案正在進(jìn)行是為了把這些系統(tǒng)和交互式定理證明器相連。這是極其有價(jià)值的工作：如果知道一個(gè)一階的陳述是可證明的，這時(shí)應(yīng)該期待機(jī)器能提供一個(gè)證明。 在這一節(jié)中，我們簡(jiǎn)略說(shuō)明一些我們已經(jīng)在各種不同的情況應(yīng)用研究的技術(shù)。自然地我們不企圖僅此一次去解決自動(dòng)化推論的問(wèn)題。寧可我們把重心集中在問(wèn)題，而這些問(wèn)題典型地出現(xiàn)在我們已經(jīng)涉及的研究。我們首先簡(jiǎn)略說(shuō)明我們需要的自動(dòng)化的引擎功能。我們?nèi)缓竺枋鑫覀儜?yīng)用的技術(shù)，而且他們是如何整合的。我們?cè)u(píng)估根據(jù)我們的需求性質(zhì)上地產(chǎn)生的引擎，和數(shù)量地有關(guān)于一件相當(dāng)大的案例研究。這些技術(shù)中的少數(shù)是新奇的，寧可，我們企圖用一種適宜的方式來(lái)融合現(xiàn)行的技術(shù)。 這些步

15、驟在HOL啟發(fā)定理證明器被開(kāi)展，這是我們建立的設(shè)計(jì)原型的一輛優(yōu)良車輛的不同方法。 2 需求 我們的自動(dòng)化的需求是什么? 讓我們區(qū)別一下自動(dòng)化和全自動(dòng)化的使用，以及交互式自動(dòng)化的使用，每一種的需求都有非常地不同。 也許料想不到地，失敗的自動(dòng)化證明引擎是基準(zhǔn)，是觀念，這觀念是當(dāng)交互式開(kāi)展的復(fù)雜證明使我們花費(fèi)大多數(shù)時(shí)間對(duì) " 幾乎 " 的可證明的義務(wù)的時(shí)候。因此我們想要證明器給我們完美的反響作為為什么任務(wù)不能夠被執(zhí)行的原因。 這引證強(qiáng)調(diào)一種在自動(dòng)化和交互式證明之間的重要的不同。在自動(dòng)校對(duì)中，可典型地知道，目標(biāo)是可證明的 ( 或至少，非常強(qiáng)烈地疑心，而且在結(jié)束相當(dāng)多量的時(shí)間之前準(zhǔn)備等候證

16、明的搜尋)。確實(shí)，自動(dòng)證明器被判斷在他們能實(shí)際上證明多少可證明的目標(biāo)之上。在交互式證明中，" 我們花費(fèi)我們大多數(shù)的時(shí)間在幾乎可證明的義務(wù)上"。這是交互式和證明之間的不同。如果我們花費(fèi)大部份的時(shí)間嘗試去證明簡(jiǎn)單但不可證實(shí)的目標(biāo)，然后校正的搜尋完全變成比擬不重要。這雖不能說(shuō)是它全部失去重要:：如果一個(gè)系統(tǒng)缺乏完整性，這時(shí)它將會(huì)無(wú)法證明一些可證明的目標(biāo)。什么類型的目標(biāo)正在被放棄，這是非常必要而且主要去知道的，這是為了知道當(dāng)一個(gè)證明器失敗于證明一個(gè)目標(biāo)時(shí)就能理解它是什么意思。這些知識(shí)也非常有用，當(dāng)混合系統(tǒng)為了了解作為整個(gè)系統(tǒng)的行為，應(yīng)當(dāng)首先了解局部的行為。 在一個(gè)交互式的環(huán)境中，在完全之上所有物可能

17、被偏愛(ài)，就我們而言，自動(dòng)化的最重要方面是簡(jiǎn)單化。 而這些我們不是意味著去落實(shí)簡(jiǎn)單 ( 要布多少根線來(lái)實(shí)現(xiàn)系統(tǒng)? 等等)，而是概念上的簡(jiǎn)單化。例如，簡(jiǎn)單化到處被用于交互式定理求證。如果一組改寫(xiě)規(guī)那么不能融合，這時(shí)去了解簡(jiǎn)化器的行為，必須了解適用的規(guī)那么順序。不用說(shuō)，對(duì)于理解這是一件極端復(fù)雜的事情，而且屬于這些所有物的證明在推測(cè)上極端易碎。概念上的簡(jiǎn)單化通過(guò)聚集和簡(jiǎn)易裝置的終端對(duì)一個(gè)簡(jiǎn)化器進(jìn)行緊密地約束。如果一個(gè)使用者要了解系統(tǒng)，概念上的簡(jiǎn)單化很重要。如果一個(gè)系統(tǒng)的概念簡(jiǎn)單，它將會(huì)很有希望被簡(jiǎn)單的使用。 在一個(gè)交互式環(huán)境中，我們期待自動(dòng)化失敗。為了取得進(jìn)步，我們必須了解一種證明的嘗試為什么失敗，

18、證明器一定會(huì)提供反響?；谙到y(tǒng)的決議能提供反響，但是他們是消滅性的 (在某種意義上目標(biāo)轉(zhuǎn)換成一種正常的形式在證明的嘗試之前開(kāi)始，破壞了最初的邏輯結(jié)構(gòu))，所以反響很難被了解 (論證失敗的點(diǎn)對(duì)于最初的目標(biāo)能看出明顯的不同)。較好的方式是引導(dǎo)在一個(gè)盡可能接近的方法證明到一個(gè)人類可能如何引導(dǎo)證明。在一些感覺(jué)中我們需要證明的系統(tǒng)應(yīng)該是自然的。在這情況下，如果一種證明的嘗試失敗，失敗的局部能時(shí)常被作為檢驗(yàn)直接地返回給使用者。 反響與能見(jiàn)度相關(guān)。時(shí)常一個(gè)使用者希望檢查失敗的證明，但是只有證明的蹤跡是可得的，它能引起一個(gè)概念上的錯(cuò)誤結(jié)合: 使用者把重心集中在結(jié)果，然而蹤跡可能全部是有不同的自然。如果有許多沒(méi)

19、有被證明的局部，這時(shí)一個(gè)使用者不可能檢查它們的全部，但是可能愿意沿著證明走。像約翰 哈里森的模式消除的執(zhí)行的自動(dòng)化方法，時(shí)常利用全球化的節(jié)點(diǎn)優(yōu)先尋址的信息在一棵樹(shù)里搜尋一個(gè)證明。如果全球化的信息不是出現(xiàn)在結(jié)果中使用者有時(shí)機(jī)接近，它將會(huì)難以經(jīng)過(guò)通過(guò)簡(jiǎn)單運(yùn)用的自動(dòng)證明器一步一次的自動(dòng)化證明。當(dāng)傳導(dǎo)的搜尋正在使用全球化的信息時(shí)，自動(dòng)證明器將不做出它做出的相同決定，因?yàn)樗荒苓M(jìn)入本地的結(jié)果。 許多方法現(xiàn)在被交互式定理證明器所使用，就像伊莎貝爾的blast，留下未改變的目標(biāo)如果它們失敗于證明這目標(biāo)的話。證明搜尋的自然方法期待在所有的情形中至少能做出一些進(jìn)步，所以即使目標(biāo)不是可證明的，它們也能夠有所幫助

20、。 比方，平安的步驟 (就像在許多系統(tǒng)的∧E) 應(yīng)該被實(shí)行，簡(jiǎn)單化步驟被應(yīng)用等等。 自動(dòng)化也應(yīng)該是穩(wěn)定的。在大量的證明中，一個(gè)證明時(shí)常混合交互式和自動(dòng)的證明。如果被自動(dòng)化返回的目標(biāo)容易根本地以目標(biāo)的微小變化改變，這時(shí)關(guān)聯(lián)的交互式證明將被毫無(wú)用處的給予，而且一定被改寫(xiě)。因?yàn)檫@一個(gè)理由，被自動(dòng)化返回的不能解決的次目標(biāo)應(yīng)該在對(duì)于最初的目標(biāo)的微小改變下穩(wěn)定。 如果一個(gè)證明能被建立，然后一開(kāi)始把重心集中在使證明更加可維持的方面，就像魯棒一樣。效率是在蛋糕上的糖衣。完全也是重要的，雖然沒(méi)有必要在一階邏輯完全，但是寧可應(yīng)該有一個(gè)給定的程序解決的層次問(wèn)題一個(gè)清楚的觀念。無(wú)論如何，一些系統(tǒng)的行為理論上理解是

21、重要的，如果它接近簡(jiǎn)單的目標(biāo)。 讓我們總結(jié)出這些觀點(diǎn)： ? 自動(dòng)化應(yīng)該很簡(jiǎn)單：它應(yīng)該在理論上很好地被了解，和在使用中可預(yù)期的。 ? 自動(dòng)化也應(yīng)該提供反響，以至于使用者能估定一種證明的嘗試為什么失敗。 ? 一個(gè)甚至比擬強(qiáng)烈的需求是，自動(dòng)化是可視的，在可視中通過(guò)證明的研究，能直接地檢查自動(dòng)化的執(zhí)行。 ? 自動(dòng)化應(yīng)該是自然的，這是為了使證明器和使用者之間的概念差距最小化。舉例來(lái)說(shuō)，自動(dòng)化應(yīng)該在標(biāo)準(zhǔn)的邏輯系統(tǒng)中執(zhí)行，或者與使用者傳導(dǎo)證明的決策程度相一致。 ? 時(shí)常，使用者對(duì)一個(gè)證明進(jìn)行優(yōu)化有很多的平安步驟。與自動(dòng)化在返回前至少做出改良相比，自動(dòng)化簡(jiǎn)單的返回“可證明〞與“不可證明〞是沒(méi)什么用

22、處的。 ? 自動(dòng)化應(yīng)該是穩(wěn)定的，以至于在自動(dòng)化的行為中理論上微小的改變不會(huì)產(chǎn)生大的變化。這是很重要的，因?yàn)榻换ナ降淖C明包含大量隔行掃描使用者或自動(dòng)化步驟的環(huán)節(jié)。 ? 自動(dòng)化也應(yīng)該是魯棒的，在意義上微小的變化不會(huì)影響自動(dòng)化的可證實(shí)性。 ? 我們想要自動(dòng)化對(duì)明顯的理論是有效率的。 ? 最后，我們想要自動(dòng)化是完全精密的。她能很好的定義問(wèn)題的層次。 3 目前交互式證明器的自動(dòng)化 目前交互式定理證明器的自動(dòng)化證明方法不符合先前環(huán)節(jié)的需求。 Isabelle/ HOL是目前作為被認(rèn)可的HOL執(zhí)行的代表。 主要被使用的技術(shù)是一個(gè)描述的證明器blast，和簡(jiǎn)化器simp。這些都混合在單個(gè)的

23、自動(dòng)化策略里。 Isabelle也包括一個(gè)模式消除程序，它和blast使用起來(lái)有點(diǎn)相似。 Simp 被廣泛地使用，但是它并不是一個(gè)完全的一階證明方法。然而，它能滿足許多前期環(huán)節(jié)需求的事實(shí)解釋了為什么它這么流行，在交互式證明中。blast方法在肯定邏輯和組的簡(jiǎn)單問(wèn)題上運(yùn)行得很好，但是它很難了解它的特性是什么。它基于一個(gè)證明器leanTAP，那對(duì)一階邏輯是完全的。另一方面，以下的目標(biāo)稍微可證明在一階邏輯，但是blast不行。 f( g a)=a┝З y ?g(f y)=y 它甚至更加的混亂，但它在區(qū)間 g a 實(shí)現(xiàn)的時(shí)候，這區(qū)間在結(jié)果本身中發(fā)生，并是存在的證明。更糟的是，當(dāng)像HOL 的類型邏

24、輯被表達(dá)的時(shí)候，g a 是唯一的區(qū)間發(fā)生在可以使用的正確類型結(jié)果中。這一個(gè)失敗對(duì)于有效地處理等式邏輯是一個(gè)描述類型程序失敗的合并統(tǒng)一。因?yàn)樗沁@么的不受限制，所以自動(dòng)方法幾乎從不被用于交互式證明的中間。而且，它是不穩(wěn)定的，在它產(chǎn)生的子目標(biāo)中在對(duì)目標(biāo)的較小變化之下可能是野性地不同的，它的提出是無(wú)用的除了在緊緊地被控領(lǐng)域。 整合一個(gè)現(xiàn)代的解決證明器Vampire進(jìn)入Isabelle將沒(méi)有必要糾正這些錯(cuò)誤?；诮鉀Q的方式提供了一點(diǎn)支持對(duì)于交互式理論證明器，因?yàn)樽泳湫问降臏p少意味著使用者有很少的可觀性進(jìn)入證明的搜尋，而且很少知道為什么一個(gè)特殊的輔助定理會(huì)失效。證明的搜尋是一個(gè)本地的向前的綜合的搜尋，

25、與一個(gè)全球化的向后的綜合搜尋的典型描述介紹以及Isabelle的策略水平相反。因此，對(duì)于使用者，解決是一個(gè)不自然的系統(tǒng)。通常從這些系統(tǒng)來(lái)的反響是極差的甚至不存在的。此外，許多步驟應(yīng)該被認(rèn)為是平安的 (應(yīng)用一個(gè)終端和聚合的改寫(xiě)組，運(yùn)行一個(gè)∧ E 步驟) 因?yàn)橄到y(tǒng)被當(dāng)作一個(gè)黑盒子使用，或目標(biāo)率直地被解決，或者更通常，一點(diǎn)也不解決，而且系統(tǒng)包含的關(guān)于可靠應(yīng)用的步驟被喪失的信息，留給使用者可以手動(dòng)的應(yīng)用這些步驟。這里的問(wèn)題是系統(tǒng)無(wú)法做出改良那些無(wú)法直接證明的目標(biāo)。 我們也作關(guān)于一階理論證明器的以下觀察。這些證明器被設(shè)計(jì)去尋找大量的數(shù)量詞實(shí)例，尋找可選擇地系數(shù)平等推論。然而在交互式定理證明器里的自動(dòng)化

26、的失敗沒(méi)有失敗于猜想大量的數(shù)量詞實(shí)例。 4 技術(shù) 在下面這節(jié)，我們描述我們?nèi)绾谓⒆詣?dòng)化。首先，我們正在嘗試尋找證明，所以我們將會(huì)需要 ( 至少) 證明的搜尋引擎。然后，我們?cè)诤艽蟮某潭壬显缸鲇檬謩?dòng)的方式的模型證明。除了證明的搜尋之外，在手動(dòng)證明中其他主要的利用方法是簡(jiǎn)單化。我們描述我們?cè)鯓佑懻摵?jiǎn)化器。 有條件的簡(jiǎn)單化是一種簡(jiǎn)單化的形式，它的簡(jiǎn)化器采用遞歸的方式企圖解決可能被應(yīng)用的當(dāng)前目標(biāo)的改寫(xiě)選擇。我們討論正采用在這些目標(biāo)上的簡(jiǎn)化器沒(méi)有被最好的運(yùn)行，并建議替代選擇。 然后，當(dāng)使用簡(jiǎn)單化的時(shí)候，它是一個(gè)很好的方法去確定簡(jiǎn)單裝置是集合的和終端的。我們描述完成的執(zhí)行。當(dāng)使用簡(jiǎn)單化的時(shí)

27、候，然而，也想利用在改寫(xiě)一個(gè)證明的過(guò)程中產(chǎn)生的假設(shè)。確定改寫(xiě)規(guī)那么的組仍然是聚合的和終止的，就應(yīng)該在證明搜尋時(shí)提供一些動(dòng)態(tài)完成的形式。我們討論我們?nèi)绾巫プ×诉@些議題。 4.1證明的搜尋 在這節(jié)中，我們描述我們證明搜尋的根本系統(tǒng)。這是一個(gè)單一的結(jié)論，對(duì)向后的證明搜尋是適當(dāng)?shù)闹庇^系統(tǒng)。我們避開(kāi)統(tǒng)一的流行的區(qū)間計(jì)算。這有一些有趣的結(jié)果當(dāng)混合證明搜尋時(shí)用其他的方法。注意我們只對(duì)自動(dòng)化的一階系統(tǒng)感興趣。 邏輯系統(tǒng) 證明搜尋的二個(gè)主要系統(tǒng)是決議和描述。因?yàn)橐粋€(gè)交互式環(huán)境的自動(dòng)化，決議太不自然。因?yàn)檫@一原因，描述是更有希望的。我們因此限制我們的注意在基于描述的系統(tǒng)。描述系統(tǒng)典型地藉由否認(rèn)目標(biāo)

28、而且尋找矛盾著手進(jìn)行。我們甚至考慮到這是不自然的。我們因此集中在標(biāo)準(zhǔn)邏輯系統(tǒng)中直接執(zhí)行的描述系統(tǒng)。 使用這樣一個(gè)系統(tǒng)根據(jù)復(fù)雜的執(zhí)行有重要的意義，因?yàn)槲覀兡苤皇呛?jiǎn)單地在 HOL 目標(biāo)的水平搜尋使用或多或少標(biāo)準(zhǔn)的策略。這也對(duì)自然化有有利條件，因?yàn)槭褂谜咭呀?jīng)熟悉一個(gè)如此系統(tǒng)的證明和反響，因此我們能直接地對(duì)使用者呈現(xiàn)失敗的局部，這些使用者沒(méi)有翻譯出來(lái)自一些其它可能的證明系統(tǒng)的結(jié)果。 單一結(jié)論系統(tǒng)對(duì)古典的證明是不適宜的，古典的證明被多樣結(jié)論系統(tǒng)更好的支援。然而多樣的結(jié)論系統(tǒng)是不自然的。如果我們對(duì)古典的證明感興趣，我們一定成認(rèn)我們的單一結(jié)論系統(tǒng)有缺點(diǎn)。另一方面，我們相信大規(guī)模的證明結(jié)構(gòu)大概是直觀的：我

29、們典型地集中于一個(gè)目標(biāo)，并且我們的輔助定理效勞作為證明中的中間觀點(diǎn)，和我們的補(bǔ)助定理如證明的中間點(diǎn)效勞，即├A?B→ C作為一個(gè)補(bǔ)助定理對(duì)├ ┑(A ? B ) ?C不是典型地相等，因此我們期待在證明中到達(dá)一個(gè)點(diǎn)，這里A ? B 是可證明的，而不是去做一個(gè)可分的拆開(kāi)。確定地對(duì)于我們感興趣的領(lǐng)域，所有的證明本質(zhì)上是直觀的，以及古典的推論被限制到可能被簡(jiǎn)單化或其他的限制技術(shù)處理的小區(qū)域。 引進(jìn)規(guī)那么 我們希望做出更多的進(jìn)步。雖然程序簡(jiǎn)述說(shuō)明上方是完全的，它寧可是一邊的。既然大多數(shù)的證明大量利用輔助定理，對(duì)應(yīng)的目標(biāo)傳輸容易變成相當(dāng)擁擠。而且，當(dāng)引進(jìn)規(guī)定的時(shí)候，許多輔助定理自然地被瀏覽，也就是

30、說(shuō)，趨于使用精煉的結(jié)論 C 而不愿使用從Г開(kāi)始向前連接著的結(jié)論。因?yàn)檫@些理由，我們也利用引進(jìn)規(guī)那么à la Paulson[PNW03]。這些典型不平安，但是如果我們?cè)僖淮畏祷?，而且輪流其他的防范，完全性就能被保存。這些引進(jìn)規(guī)那么能像輔助定理一樣被執(zhí)行，但是被作記號(hào)作為引進(jìn)規(guī)那么。在證明的搜尋時(shí)候，這些輔助定理的結(jié)論被相配對(duì)抗當(dāng)前的目標(biāo)。如果結(jié)論與當(dāng)前的目標(biāo)相配，那么目標(biāo)將被選擇的引進(jìn)規(guī)那么所代替，而且在事件中這些假定不能夠被證明，那么返回將被采用。如果一條引進(jìn)規(guī)那么標(biāo)明是平安的，這時(shí)返回不發(fā)生。注意，這些提高沒(méi)有必要來(lái)自理論的觀點(diǎn)，而且它的唯一動(dòng)機(jī)是做模型自然形式的證明。 如果完全性以特定

31、的方式被考慮，這時(shí)候能夠看見(jiàn)完全性的保存。如果這些規(guī)那么是行為表現(xiàn)所預(yù)期的，那么在簡(jiǎn)單化之前需要等式的統(tǒng)一。然而，目前我們用手動(dòng)的方式來(lái)模擬等式統(tǒng)一的使用。 完全性失敗對(duì)于引用規(guī)那么：如果我們以一條規(guī)那么作為一條引進(jìn)規(guī)那么，這時(shí)我們無(wú)法是完全的? 不過(guò)這不是真實(shí)的，而且規(guī)那么是平安的，在哪一情況我們都很順利，或不平安的，在哪一情況我們返回。需求的統(tǒng)一意味著我們能防止我們能防止作為增加的假設(shè)而使用的規(guī)那么。然而，如果在一些階段我們能以規(guī)那么作為一條引進(jìn)規(guī)那么，這里有一個(gè)引進(jìn)規(guī)那么被打算使用的環(huán)境，但是沒(méi)有連接鏈，然而當(dāng)一項(xiàng)額外的假定可能有時(shí)這里將沒(méi)有統(tǒng)一的問(wèn)題。 而且，自從我們沒(méi)有使用一個(gè)作

32、為標(biāo)準(zhǔn)的輔助定理的規(guī)那么，使用完全化的概念將不是很清楚。讓我們定義完全化的生產(chǎn)一個(gè)引進(jìn)規(guī)那么去了解是否有一個(gè)證明作為一個(gè)輔助定理的規(guī)那么。這時(shí)一個(gè)使用規(guī)那么的證明作為一條引進(jìn)規(guī)那么。在平等面前，我們應(yīng)該因此使用統(tǒng)一去確定我們的引進(jìn)規(guī)那么能被無(wú)論在那里都可能應(yīng)用。既然在每個(gè)階段我們有一個(gè)有限的場(chǎng)地區(qū)間組，與一個(gè)終端和集合的改寫(xiě)次序，這樣一個(gè)方法能夠可以實(shí)行，即使在現(xiàn)階段我們只能用人工模擬這樣的步驟。 引進(jìn)規(guī)那么的使用會(huì)帶來(lái)復(fù)雜化，因?yàn)橥耆欠襁m合不清楚。如果引進(jìn)規(guī)那么能作為一個(gè)正常的輔助定理使用，這時(shí)完全化是可以保存的，因此輔助定理被操作就像它是個(gè)正常的肯定邏輯。在一條引進(jìn)規(guī)那么后面的方案是

33、去平衡證明的搜尋，這會(huì)以別的方式主要地在左邊上操作。在規(guī)那么├ A → B作為幾個(gè)輔助定理和作為一個(gè)引進(jìn)規(guī)那么之間的差異，是自動(dòng)化能應(yīng)用→ L與一個(gè)作為輔助定理的規(guī)那么相結(jié)合。因此作為一個(gè)引進(jìn)規(guī)那么，我們期望目標(biāo)最終成為B和它能用A代替這些。 4.2 等式 改寫(xiě) 改寫(xiě)是由用相等的子術(shù)語(yǔ)更換一個(gè)術(shù)語(yǔ)的變換過(guò)程。例如，我們可能使用輔助定理f (a) = a去改寫(xiě)Q f (f (a)) 到 Q f (a)然后到Q (a)。在這節(jié)中，我們的各種改寫(xiě)概念是非正式的。對(duì)于更多的信息讀者可以請(qǐng)教優(yōu)秀者。 在用辭上的一個(gè)注解：一個(gè)簡(jiǎn)單化的次序是一個(gè)改寫(xiě)被限制的次序，過(guò)去一直用來(lái)證明一個(gè)區(qū)間改寫(xiě)系統(tǒng)

34、的終止。然而，“簡(jiǎn)單化〞這個(gè)詞時(shí)常被非正式地用于提到改寫(xiě)，而且“ 簡(jiǎn)化組〞這個(gè)詞時(shí)常用來(lái)提及改寫(xiě)的系統(tǒng)規(guī)那么。我們下面采用這些非正式的用法。 兩個(gè)主要的簡(jiǎn)單化財(cái)富是終止和聚集。沒(méi)有聚集，了解簡(jiǎn)化器的行為就必須知道改寫(xiě)被應(yīng)用的次序。這太多而不是使用者所期待的。在一個(gè)交互式環(huán)境中終止非常有用，例如，它允許反響。而且，終止允許簡(jiǎn)單化與主要的證明的搜尋相整合。如果我們有聚集和終端，這時(shí)每一個(gè)區(qū)間有一個(gè)獨(dú)特正式形式，而且嘗試的等式變得可決定。這是一個(gè)極其有用的簡(jiǎn)化組的財(cái)富。 我們的根本策略是熱心地應(yīng)用簡(jiǎn)單化，在證明的搜尋每個(gè)步驟之后，使用假定去簡(jiǎn)化其他的假定和結(jié)論。我們用一個(gè)有終止和聚集的簡(jiǎn)化器工作

35、。我們檢查終止和聚集的手動(dòng)使用完成。我們?cè)趥€(gè)體的類型中應(yīng)用簡(jiǎn)單化。如果簡(jiǎn)化組正在終止和聚合，這時(shí)它保存了證明搜尋的完全性。我們也在布爾類型應(yīng)用簡(jiǎn)單化，但它不是一階邏輯的一種可能性。例如，我們采用高階對(duì)微小范圍的數(shù)量詞改寫(xiě)。不是太困難而無(wú)法爭(zhēng)論而這也保存證明的搜尋完全。經(jīng)常相似改寫(xiě)的假定在證明期間出現(xiàn)，而且這些可能被簡(jiǎn)化組合并。給一項(xiàng)假定x.P x和假定 P t，就可以簡(jiǎn)化 P t=，是再一次在布爾類型的簡(jiǎn)化，而不是一階的操作。我們不以這一種形式的假定作為改寫(xiě)：我們的對(duì)數(shù)量詞例如的根本途徑經(jīng)由區(qū)間計(jì)算，而且使用這些簡(jiǎn)單化會(huì)破壞這方式的完全。我們使用假定形式x= y(可能數(shù)量化)來(lái)改寫(xiě)。 為了保有

36、聚集和終止，我們完成簡(jiǎn)化組的生產(chǎn)并動(dòng)態(tài)的產(chǎn)生改寫(xiě)。因?yàn)橥瓿蓻](méi)被保證結(jié)束，完成被限制到一個(gè)步驟確實(shí)定數(shù)字，雖然在我們的應(yīng)用中，完成總是成功。 條件的簡(jiǎn)單化 在這節(jié)中，我們描述有條件的簡(jiǎn)單化，并且注意到標(biāo)準(zhǔn)的途徑去解決遞歸環(huán)境下簡(jiǎn)化器的實(shí)施可能沒(méi)有被期待。我們建議一些其他的方法，而且討論其他的有條件的簡(jiǎn)單化的問(wèn)題。我們得出結(jié)論，目前有條件的簡(jiǎn)單化太復(fù)雜而無(wú)法作為 " 簡(jiǎn)單的 " 技術(shù)計(jì)算，并且確實(shí)太復(fù)雜而無(wú)法以一合理的方式與證明的搜尋相連接。我們建議考慮有條件的改寫(xiě)就如平常的輔助定理的一樣的替代選擇。 簡(jiǎn)單化的工作在于對(duì)形式a = b的改寫(xiě)，在目標(biāo)的任何地方改寫(xiě)a到 b。有條件的簡(jiǎn)單化的

37、工作在于對(duì)有條件的形式├A→a = b〔A是一典型的連接〕的改寫(xiě)。在一個(gè)依次的Г├ C 中，如果我們能證明﹃C, Г的話，我們就能在目標(biāo)里調(diào)整a到b的改寫(xiě)。 我們應(yīng)該如何嘗試去證明條件A? 假設(shè)我們正在用簡(jiǎn)單化連接一個(gè)完全的證明搜尋系統(tǒng)。在這情況下，非常好的 (從一個(gè)理論上的立場(chǎng)) 行為會(huì)被由需求獲得，如果A是可證明的，那么它實(shí)際上是被證明的。因?yàn)閷?duì)A的證明的搜尋是潛在的沒(méi)有終止的，我們這時(shí)應(yīng)該妥善地安排一個(gè)復(fù)雜的隔行掃描主要證明搜尋的過(guò)程，與子證明搜尋企圖去解決有條件的改寫(xiě)情況。一個(gè)如此方式是不適口的不只因?yàn)樾实脑颉? 簡(jiǎn)單化的好處之一是，不像證明的搜尋，它正在終止。如果當(dāng)采用有條件的

38、簡(jiǎn)單化的時(shí)候，我們希望保存這一終止的行為，當(dāng)企圖證明條件的時(shí)候，我們應(yīng)該遵行被涉及的非終止。一個(gè)我們應(yīng)該采用的主要證明搜尋是去證明條件，但是限制對(duì)特別深度的搜尋。這也是不適口的。為了在一個(gè)合理的時(shí)間里保持簡(jiǎn)單化的運(yùn)行，這深度應(yīng)當(dāng)非常小，因?yàn)闂l件的產(chǎn)生是很頻繁的。這些小的深度不能提供更多的條件解決方法比其他簡(jiǎn)單的方法。對(duì)于一個(gè)小深度的有限制的證明搜尋，這也意味著它的理論限制也能成為實(shí)際的限制：任何的有限制的證明搜尋將會(huì)是不完全的，但是由于大的深度我們可以有希望的忽略這樣的不完全。小的深度意味著我們可能面臨的條件能被解決的條件，這條件對(duì)于使用者是很清晰的，不過(guò)被限制的搜尋深度意味著情況沒(méi)有被解決。

39、根據(jù)我們的經(jīng)驗(yàn)，深度必須至少有10個(gè)邏輯的步驟 ( ∨ E 及其他。)，連接中間有效的等式推論(我們想像一個(gè)情節(jié)我們有一個(gè)有效地處理等式的證明搜尋)。在實(shí)驗(yàn)方面，根據(jù)簡(jiǎn)化器的反響時(shí)間執(zhí)行這些方法變得不實(shí)際，在深度4之后。在將來(lái)，這些方法對(duì)于電腦將變得是可實(shí)行的，雖然目前它不能。 一個(gè)使用有限制的證明搜尋的替代選擇是為了解決從一個(gè)條件去確定一個(gè)可接受的條件類別，而且接受一些將會(huì)有可能是可證明的條件，但是它將會(huì)在外部被給的類別上失敗。明顯的選擇是提議的邏輯。然而，有條件的簡(jiǎn)單化的問(wèn)題擴(kuò)充多深入地超過(guò)偶然的失敗證明一種提議有效的條件，如同我們稍后討論一樣，所以這方式不能產(chǎn)生任何很大實(shí)際的效益，雖

40、然行為會(huì)至少在理論上有好的理解。 被采用的 HOL ， HOL 啟發(fā)和 Isabelle 的目前方式，是在條件上激發(fā)簡(jiǎn)單器它自己。這些遞歸的召集是潛在的非終止 (有條件的簡(jiǎn)單化極端地傾向于成環(huán))，以至于被激發(fā)的遞歸簡(jiǎn)化器的時(shí)間是限制的。這些深度搜尋的限制當(dāng)解決條件遭受同樣的問(wèn)題，這些問(wèn)題在先前的段落被討論過(guò)的。方式在許多方面比上面的很差，因?yàn)轭~外的簡(jiǎn)單化所有物有必要了解它的行為，當(dāng)解決條件時(shí)，可能是不清晰的甚至在提議的條件上，讓單獨(dú)的情況來(lái)涉及述語(yǔ)。對(duì)于一個(gè)典型的目標(biāo)，我們只需要簡(jiǎn)單化能在一個(gè)簡(jiǎn)單了解的方法方面有進(jìn)步。對(duì)于條件，我們的需求通常是體檢可能的話，就被解決。簡(jiǎn)單化不是完全形式的證明

41、，因此，我們希望，我們的情況將會(huì)是以致于那簡(jiǎn)單化能經(jīng)常很好地運(yùn)行。然而，簡(jiǎn)單化不能夠證明所有的前置詞條件以至于它的行為甚至在提議的水平是難了解的。在數(shù)量詞推論上，甚至在最根本的水平，失敗是基準(zhǔn)。 因此，當(dāng)求證條件時(shí)，目前的方法無(wú)法足夠地以非終止的問(wèn)題處理。而且條件的級(jí)別可被簡(jiǎn)單化解決的很難去描述，而且不是簡(jiǎn)單的適合使用者去理解。 完成 完成是一個(gè)能確定簡(jiǎn)單組是聚合還是終止的程序。聚合與終止是我們要求簡(jiǎn)化組具備的兩個(gè)主要所有物，所以完成是當(dāng)采用簡(jiǎn)單化時(shí)一個(gè)有用的工具。我們討論我們的完成使用。 在群的公理理論上使用完成的標(biāo)準(zhǔn)例子，源自一組終止和聚合的改寫(xiě)對(duì)于這一個(gè)理論構(gòu)成一個(gè)標(biāo)準(zhǔn)的改寫(xiě)

42、系統(tǒng)的規(guī)那么，展示了完成是有力的技術(shù)。在我們的工作中，這樣的動(dòng)力是從不被需要。我們實(shí)現(xiàn)了我們發(fā)現(xiàn)的非常有用的根本完成。因?yàn)槲覀兊男枰潜幌拗频模覀儧](méi)有實(shí)現(xiàn) Huet 的完全完成程序，雖然在不同的設(shè)定中這是令人想要的。我們放下這些是為了將來(lái)的工作。 我們的完成程序也允許有條件的完成。當(dāng)工作在一個(gè)鍵入設(shè)定的時(shí)候，時(shí)常希望在一個(gè)給定的類型中提及個(gè)體的一個(gè)子集。然后介紹一個(gè)述語(yǔ)的子類型，而且限制語(yǔ)句只談?wù)撟宇愋偷慕M成。 動(dòng)態(tài)的完成 我們先前提到了它時(shí)常是一個(gè)希望以假定作為改寫(xiě)的例子。清楚地說(shuō)，假定是動(dòng)態(tài)的并且在證明的程序中各處改變。雖然我們可能開(kāi)始就錯(cuò)在改寫(xiě)的簡(jiǎn)單化規(guī)那么的組，如果我們使用

43、假定，它可能很好的作為我們的根本簡(jiǎn)化組，增大假定，不再是聚合和終止。如果我們?cè)副４嬉粋€(gè)正在共同聚合和終止的簡(jiǎn)化組的所有形式，這時(shí)我們?cè)谧C明的過(guò)程期間必須運(yùn)行一些完成形式。我們需要這樣的動(dòng)態(tài)完成，因?yàn)樗欢茉谧C明的過(guò)程期間被很好地運(yùn)行。 不幸地是，完成是一個(gè)相當(dāng)昂貴的過(guò)程。而且，它大體上非終止的。然而，當(dāng)看到各種規(guī)那么類型被使用的時(shí)候，典型地它們是一種非常簡(jiǎn)單的形式。舉例來(lái)說(shuō)，我們時(shí)常獲得與假定類似的a = b ∨ a = c，然后著手進(jìn)行一個(gè)可分的除去。 產(chǎn)生的目標(biāo)有假定a = b 和 a = c，我們?cè)缸鳛楹?jiǎn)單化的規(guī)那么來(lái)使用它。多數(shù)的這些簡(jiǎn)單化規(guī)那么是根底的。在這情況下，完成被保證去結(jié)

44、束，應(yīng)該有一個(gè)方法發(fā)生短路的完成程序去得到一個(gè)能更快速地運(yùn)行的相等程序。希望，如果我們能微小地減少完成的一條到另外一條規(guī)那么的改寫(xiě)，這時(shí)希望改寫(xiě)程序相對(duì)地充分運(yùn)用( 當(dāng)然地，這是伊莎貝爾空想的簡(jiǎn)單化的情形，而且 HOL 光簡(jiǎn)單化也在某些程度上是充分運(yùn)用的) ，而且執(zhí)行將會(huì)是可接受的。 有一些文件覆蓋了根本區(qū)間的完成。我們看 [GNP +93]。這一個(gè)運(yùn)算法那么帶來(lái)了一個(gè)根本的改寫(xiě)規(guī)那么組，而且在多項(xiàng)式產(chǎn)生一個(gè)減少的權(quán)威改寫(xiě)系統(tǒng)的時(shí)間。不幸地是，雖然過(guò)程在多項(xiàng)式時(shí)間里操作，但是它利用適宜的終止。適宜的終止在HOL啟發(fā)或Isabelle 中沒(méi)有被執(zhí)行，而且在及時(shí)上可能有一個(gè)沒(méi)有充分運(yùn)用的版本相對(duì)

45、緩慢是多項(xiàng)式的(即，雖然來(lái)自[ GNP+93] 的運(yùn)算法那么是多項(xiàng)式的在及時(shí)上，這里會(huì)有一個(gè)比例的高常數(shù))。當(dāng)然，在證明期間做一個(gè)增加的變化給等式組，因此，在這某種程度希望有一點(diǎn)提高，但是我們?nèi)匀粦?yīng)該有能夠做更多的感覺(jué)。 看一下我們使用作為改寫(xiě)的假定，它是清楚，超過(guò)根本的，他們甚至有比擬簡(jiǎn)單的自然：沒(méi)有左手邊的子區(qū)間被用于任何其他的改寫(xiě)規(guī)那么(比方，假定a = b，全然沒(méi)有左手邊的一個(gè)適當(dāng)子區(qū)間，而且我們從沒(méi)有另一項(xiàng)假定形式a = d同時(shí)發(fā)生的情況)。在這個(gè)例子中，它足夠?yàn)榱艘S持聚合和終止，用這一條規(guī)那么改寫(xiě)所有其他的簡(jiǎn)單化規(guī)那么。如果我們需要在線完成這些沒(méi)有被滿足的條件，我們會(huì)依靠我們的

46、 (被限制的時(shí)間) 完成程序，但是在我們的個(gè)案研究中這不發(fā)生。當(dāng)在根本完成的正確證明的上下文中考慮的時(shí)候，這一個(gè)結(jié)果是清晰的。然而，在我們的個(gè)案研究期間有假設(shè)干的復(fù)雜情節(jié)，沒(méi)有這最正確化，導(dǎo)致我們的證明器花了特別久的時(shí)間。 方程式的統(tǒng)一 我們的最高水平的證明搜尋基于列舉區(qū)間上升到一個(gè)確定的區(qū)間深度。統(tǒng)一沒(méi)有出現(xiàn)在一個(gè)這樣的程序中。我們引用引進(jìn)規(guī)那么à la Paulson進(jìn)入我們的搜尋程序?，F(xiàn)在由相配對(duì)的引進(jìn)規(guī)那么對(duì)抗現(xiàn)在的目標(biāo)規(guī)那么的結(jié)論被簡(jiǎn)單的完成。 引進(jìn)規(guī)那么像其他的輔助定理被對(duì)待，作為補(bǔ)充的假定它們合并的進(jìn)入結(jié)果。不過(guò)，他們作為引進(jìn)規(guī)那么被作記號(hào)。我們用具體的例子說(shuō)明它們的

47、從區(qū)間的列舉像其他輔助定理一樣。結(jié)論通過(guò)簡(jiǎn)化器被改寫(xiě)。在證明搜尋的每個(gè)階段，我們檢查任何引進(jìn)規(guī)那么的結(jié)論是否與目前的目標(biāo)相配，而且如果因此我們以引進(jìn)規(guī)那么的條件替換目標(biāo)，返回不平安的引進(jìn)規(guī)定，這有模擬等式統(tǒng)一的效果。 5 連接與整合 在這節(jié)中我們描述在早先的章節(jié)中被簡(jiǎn)述的技術(shù)如何整合進(jìn)入一個(gè)單一戰(zhàn)略，和在這一個(gè)戰(zhàn)略和使用者之間的連接。 我們的自動(dòng)化包含一個(gè)描述的證明搜尋，藉由對(duì)固定的區(qū)間深度的數(shù)量詞實(shí)例化，以要求散布到簡(jiǎn)單化。這些應(yīng)該如何被整合? 如果簡(jiǎn)單化正在終止和聚集的，這時(shí)應(yīng)用在證明搜尋的每個(gè)步驟后的簡(jiǎn)單化的明顯策略保存完全。這是在這兩項(xiàng)技術(shù)整合后的必要觀察。 策略提供了一

48、個(gè)連接給使用者。使用過(guò)程中使用者必須表達(dá)一組終止和聚集的改寫(xiě)規(guī)那么和一組引進(jìn)規(guī)那么的過(guò)程。事實(shí)上，使用者也表達(dá)一組應(yīng)該在證明期間被考慮的輔助定理，而且這些只是被當(dāng)作先前描述與目標(biāo)陳述的合并。證明搜尋地進(jìn)行，與平安的規(guī)那么和簡(jiǎn)單化熱心地應(yīng)用，以及在不平安規(guī)那么上的返回。如果證明是不成功的，失敗局部被返回給使用者幾乎沒(méi)有平安規(guī)那么，或簡(jiǎn)單化的步驟，可能被應(yīng)用。對(duì)我們的方式一個(gè)缺點(diǎn)是結(jié)果相當(dāng)大，因?yàn)槲覀冋谔囟ǖ纳疃认旅嬗盟械?類型-正確的) 區(qū)間例示數(shù)量詞。它將有一點(diǎn)適應(yīng)使用者的連接，以使這些實(shí)例化不直接地呈現(xiàn)給使用者，但是在要求上可視的。我們離開(kāi)這更進(jìn)一步工作。 6 評(píng)估 在這節(jié)中，

49、我們討論我們的證明的過(guò)程怎樣相當(dāng)于根據(jù)在第2節(jié)中被簡(jiǎn)述的標(biāo)準(zhǔn)。我們?nèi)缓笥懻撏耆淖h題。我們沒(méi)有宣稱有一個(gè)正式的證明對(duì)完全產(chǎn)生一些問(wèn)題的類別，但是我們確實(shí)討論過(guò)程有好的所有物。我們通過(guò)設(shè)置我們的技術(shù)產(chǎn)生其他的就像分析一樣的理論證明技術(shù)。然后我們通過(guò)給出的成功例子評(píng)估實(shí)際的過(guò)程使用，而且描述過(guò)程的感覺(jué)。 6.1評(píng)估生產(chǎn)需求 我們的程序與在第2節(jié)提到的標(biāo)準(zhǔn)一起被設(shè)計(jì)。我們感到它滿足簡(jiǎn)單化的需求。在概念上，我們正在執(zhí)行一個(gè)標(biāo)準(zhǔn)直觀的證明搜尋。我們合并平安的和不平安的規(guī)那么。我們?cè)谶壿嫷乃?布爾類型)和領(lǐng)域的特性類型里使用簡(jiǎn)單化。我們的簡(jiǎn)單化規(guī)那么應(yīng)該是聚集和終止的。當(dāng)改寫(xiě)不破壞重要的所有物時(shí)

50、候，我們確信任何的假定都可以使用。我們只有在限制的它們有很好的行為的例子中使用簡(jiǎn)單 化以及有條件的簡(jiǎn)單化規(guī)那么。所有的這些觀念很容易理解的。 當(dāng)使用程序的時(shí)候，概念上的簡(jiǎn)單化導(dǎo)致簡(jiǎn)單化。我們應(yīng)當(dāng)確定我們的簡(jiǎn)化組，我們的引進(jìn)規(guī)那么組，以及與目標(biāo)相關(guān)的輔助定理。策略在策略水平運(yùn)行，因此，我們能通過(guò)激發(fā)一次一步的策略步進(jìn)經(jīng)過(guò)一個(gè)失敗的證明嘗試。既然程序是非破壞力的( 在某種意義上我們直接地搜尋使用自然減除的規(guī)那么，并非對(duì)正常的形式轉(zhuǎn)換)，我們有高水平的可視化進(jìn)入證明的搜尋。失敗局部典型地立刻被理解。平安步驟的觀念意謂，即使我們無(wú)法找到證明，我們回到使用者執(zhí)行得相當(dāng)多的我們?nèi)〉眠M(jìn)步的工作。不完全顯示

51、它本身作為一個(gè)失敗去猜想大量的數(shù)量詞實(shí)例。隨著動(dòng)態(tài)完成的失敗，不完全也能在證明搜尋期間產(chǎn)生。 簡(jiǎn)單化導(dǎo)致了穩(wěn)定性。當(dāng)在它已經(jīng)成功之前，我們會(huì)稱的證明器是單調(diào)的，在那增加的輔助定理中，簡(jiǎn)單化的規(guī)那么，或不平安的規(guī)那么不會(huì)導(dǎo)致程序的失敗。同樣地證明器是魯棒的，即使對(duì)定義有微小的變化等等。我們不會(huì)宣稱程序是有效率的。 6.2完全 我們自動(dòng)化有一些不完全的來(lái)源。FOL 的可證明性大體上是無(wú)法決定的。我們對(duì)區(qū)間集合的子集深度限制。是否有一個(gè)證明僅僅涉及到深度限制區(qū)間是現(xiàn)在可決定的，但是我們將會(huì)不可防止地失敗于找到我們的限制子集之外包括區(qū)間放置的證明。這是一個(gè)不完全的來(lái)源。然而，我們可能連續(xù)地

52、增加區(qū)間深度并且這樣來(lái)恢復(fù)對(duì)可決定性花費(fèi)的完全。 FOL 能在方程序的推論 [McK75] 中置入，所以期待等式推論說(shuō)明對(duì)通常證明搜尋的類似問(wèn)題。我們的方式是限制我們自己對(duì)終止和聚集的改寫(xiě)規(guī)那么組。因此完成可能失敗，或不可能結(jié)束，這是一個(gè)不完全的來(lái)源。而且，我們采用動(dòng)態(tài)的完成，能同樣地失敗，雖然在實(shí)踐中這不是一個(gè)問(wèn)題。然而，完成能讓使用者大量的進(jìn)行交互式處理。如果使用者確定，改寫(xiě)規(guī)那么組是聚集和終止的，而且如果動(dòng)態(tài)的完成在證明搜尋期間總是成功的，這時(shí)我們的等式操作將會(huì)是完整的。 6.3 效率 目前自動(dòng)化方法的成功很大停留在統(tǒng)一上，然而我們只有稍微地使用統(tǒng)一，當(dāng)操作引進(jìn)規(guī)那么時(shí)。根據(jù)證

53、明的搜尋，根據(jù)執(zhí)行我們的程序?qū)?huì)廣泛類似像吉爾曼這樣的前統(tǒng)一程序。舉例來(lái)說(shuō)，以下的目標(biāo)是可決定的： (xyz.P x y →P y z →P x z) → (xyz.Q x y → Q y z → Q x z) → (xy.P x y→P y x) → (xy.P x y ∨ Q x y) → (xy.P x y) ∨ (xy.Q x y) 確實(shí)，事實(shí)或一個(gè)公式的虛偽能在一個(gè)只有四種要素的模型中被評(píng)估。然而，即使這樣一個(gè)的目標(biāo)是可決定的，甚至于一些現(xiàn)代解決方法基于證明器的努力。不幸的是，我們的程序注定要花非常長(zhǎng)的時(shí)間。在防御中，這樣的目標(biāo)很少在交互式定理的證明中被碰到。如果他們被遇

54、見(jiàn)，使用者當(dāng)然可以用一個(gè)交互式的決議證明器去解決他們。 除了根本的證明搜尋之外，我們對(duì)等式推論給予特別的關(guān)注。我們?cè)谕瓿缮蠈?duì)等式結(jié)束的方式，和在各種可變的條件是滿足的。然而，如果保持這些情況，達(dá)成平等的方式或許是有效的?，F(xiàn)代的決議證明器采用無(wú)窮盡的完成，推測(cè)的行為將不再比完成一個(gè)完全存在的改寫(xiě)組有效率。 6.4實(shí)際應(yīng)用 因?yàn)樗拍詈?jiǎn)單，證明器是非常容易使用的。從一個(gè)定理到下一個(gè)定理的典型移動(dòng)，激發(fā)證明器關(guān)于簡(jiǎn)化組和預(yù)先輔助定理組的使用。如果證明沒(méi)有被建立，我們會(huì)見(jiàn)到失敗局部。這個(gè)局部通常是很容易理解的。幾乎總是(在我們的個(gè)案研究中，總是)需要增加一個(gè)簡(jiǎn)化規(guī)那么，或一個(gè)不是不重要的輔助

55、定理。如果輔助定理沒(méi)有已經(jīng)被證明就應(yīng)該取出并證明它。增加必要的規(guī)那么，程序被重復(fù)執(zhí)行，通常是成功的。大體上說(shuō)，我們沒(méi)有修整簡(jiǎn)單化規(guī)那么和輔助定理組到每個(gè)定理：這些規(guī)那么被利用取決與上下文的內(nèi)容，而且總是一個(gè)良好的主意去使用它們?nèi)绻梢缘脑?。相?duì)于這些，太多的規(guī)那么能導(dǎo)致執(zhí)行能力的降低，但是通常它正工作在一個(gè)給定的理論中，這里輔助定理的數(shù)量相對(duì)地被限制。 有時(shí)候必須用一個(gè)巧妙的區(qū)間例示一個(gè)數(shù)量詞，但是這些是自然的困難的步驟。在使用者的手段(并非檢查一些失敗的局部的表現(xiàn))下步進(jìn)的經(jīng)過(guò)證明的能力是非常有用的，而且提供很好的可視化，如果一些東西沒(méi)有正確工作的話。 我們討論完全不是首要重要的，但是清

56、楚地自動(dòng)化的目標(biāo)是協(xié)助使用者證明輔助定理。如果自動(dòng)化能直接證明輔助定理，我們將沒(méi)有抱怨的了。 在我們的個(gè)案研究中我們執(zhí)行許多證明。一個(gè)主要的結(jié)果包含超過(guò)250條交互式證明的手寫(xiě)體。這些證明的手寫(xiě)體不是最初的證明抄寫(xiě)，所以自動(dòng)化可以可實(shí)現(xiàn)的再造它們。我們的自動(dòng)化能夠解決每一個(gè)輔助定理。 我們提供針對(duì)證明的一個(gè)區(qū)段的統(tǒng)計(jì)，它涉及輔助定理 theorem_3_ nes_Mup，對(duì)于其他輔助定理是代表性的。這些輔助定理依次有一個(gè)次補(bǔ)助定理theorem_3__Mup _3。在下面的列表中，我們記錄定理名稱，策略手寫(xiě)體的組成沒(méi)有我們的自動(dòng)化，組成有我們的自動(dòng)化和花費(fèi)的時(shí)間。當(dāng)求證 theorem_3_

57、nes_Mup時(shí)，次輔助定理 theorem_3_nes_Mup_3 被提供應(yīng)自動(dòng)化。當(dāng)這個(gè)次輔助定理被省略，而且主要的輔助定理不需要theorem_3_nes_Mup協(xié)助的時(shí)候，我們也記錄發(fā)生的東西。這涉及了證明器在主要的輔助定理的證明期間的再次證明。在這情況下，一個(gè)證明被建立，雖然它需要花超過(guò)5 分鐘的時(shí)間。然而，我們相信，這是由于自動(dòng)化策略的無(wú)效率實(shí)行，而且我們想要在將來(lái)的工作中再實(shí)現(xiàn)它。這些補(bǔ)助定理對(duì)自動(dòng)化對(duì)個(gè)案研究的其他輔助定理的效果是有代表性的。而且，我們已經(jīng)在其他的領(lǐng)域中相對(duì)成功的應(yīng)用了這樣的技術(shù)。 即使執(zhí)行很差勁，調(diào)和這些證明程序以至于輔助定理能被證明是一個(gè)主要的完成。事實(shí)上

58、我們可以用一個(gè)常用的方法提供程序有很好的理論所有的證據(jù)。 定理名稱 策略行 自動(dòng)操作的策略行 自動(dòng)操作的時(shí)間/秒 theorem3_ nes_Mup _3 28 1 66 theorem3_ nes_ Mup 12 1 24 theorem3_ nes_Mup' n/a 1 305 7 替代選擇 我們開(kāi)展的自動(dòng)化被我們?cè)诎?/p>

59、例研究中遇見(jiàn)的問(wèn)題所激發(fā)。然而，我們總是能夠完成我們的簡(jiǎn)化組的事實(shí)應(yīng)該是一件幸運(yùn)的事情。大體上我們能期待完成舉例失敗對(duì)于表達(dá)交換性的規(guī)那么來(lái)說(shuō)，所以測(cè)試兩個(gè)區(qū)間經(jīng)過(guò)一個(gè)權(quán)威的改寫(xiě)組的等式。這里有一些處理問(wèn)題的環(huán)境的方法，比方順序改寫(xiě)交互式的規(guī)那么的例子，但是我們想要這個(gè)時(shí)機(jī)考慮替代選擇一般的對(duì)等式處理的途徑。 到現(xiàn)在為止，我們的證明搜尋限制了被考慮的區(qū)間深度。看起來(lái)似乎限制等式推論到一個(gè)共同的區(qū)間子集是很合理的，而且在這里面采用適合終止限制的子集。這些介紹是過(guò)程的不完全。 求證 s= t 使用等式需要的公理，大體上，是任意很大深度的區(qū)間。如果我們限制我們考慮的區(qū)間深度，我們的等式推論將會(huì)是

60、不完全的。舉例來(lái)說(shuō)，假設(shè)我們通過(guò)轉(zhuǎn)移鏈s = u = v = x = y=t來(lái)證明一個(gè)等式s = t。這樣的一個(gè)證明被展示在圖1。如果我們限制我們考慮到 d 或更小的區(qū)間深度，圖可能與圖2相似。 在這個(gè)情況下，等式s= u= v 將會(huì)被獲得，但是等式x= y 和 y= t 將不會(huì)被獲得。 如果沒(méi)有 s= t 的證明存在與被限制的共同區(qū)間里，我們將會(huì)無(wú)法推論得到s=t。 因此在任何給出的我們證明搜尋的階段，我們的等式推論將會(huì)是不完全的。然而，如果我們連續(xù)地增加我們考慮的區(qū)間深度，我們將重新獲得等式推論的完全性。 在這一環(huán)境下，方程式的統(tǒng)一，生產(chǎn)被限制的區(qū)間組，變成可決定的，而且能非常有效率地

61、實(shí)現(xiàn)。 這個(gè)方式的另一個(gè)優(yōu)點(diǎn)是給同等級(jí)別的代表能在一個(gè)使用者特別的習(xí)慣下被選擇。舉例來(lái)說(shuō)，使用者可能選擇同等類型的子句作為代表，或最小的產(chǎn)生一些詞典的路徑命令。這對(duì)使結(jié)果保持易讀有幫助。 這方式的另一個(gè)優(yōu)點(diǎn)是使用者的理解是簡(jiǎn)單的，而且我們?cè)谧C明搜尋的方法密合得很好。聚焦在單個(gè)復(fù)雜性上的衡量，比方區(qū)間深度，在一些程序之上，是一個(gè)統(tǒng)一的步驟。而且，缺點(diǎn)和方式的不完全經(jīng)由完成在這里是不存在的。我們留下這些替代選擇的執(zhí)行給將來(lái)的工作。 區(qū)間深度 s u v x y t 區(qū)間

62、 圖1: 傳遞性的等式證明 d 區(qū)間深度 s u v x y t 區(qū)間 圖2: 有深度限制的傳遞性等式證明 8 結(jié)論 我們已經(jīng)呈現(xiàn)我們開(kāi)展去抓住一件大的個(gè)案研究的自動(dòng)化。自動(dòng)化被修整到交互式的使用，自動(dòng)化以一個(gè)證明搜尋引擎和簡(jiǎn)單化的整合為根底，本質(zhì)上依賴于完成。 這節(jié)的奉獻(xiàn)是根據(jù)根本的證明搜尋，和它的簡(jiǎn)單化整合，在一個(gè)交互式假定里解說(shuō)目前自動(dòng)化的失敗。我們的技術(shù)

63、沒(méi)有走出等式術(shù)語(yǔ)邏輯的范疇，不過(guò)甚至在這樣一個(gè)被限制領(lǐng)域，我們遇到了很多的問(wèn)題。另一方面，解決這些問(wèn)題，我們沒(méi)有對(duì)特殊自動(dòng)化領(lǐng)域的需求。我們不否認(rèn)，在線性算術(shù)區(qū)域中，這樣的程序?qū)τ行У淖詣?dòng)化是很有必要的。然而，我們的經(jīng)驗(yàn)說(shuō)明簡(jiǎn)單化和證明的搜尋是一個(gè)非常有效的組合，這可能是邏輯現(xiàn)象一個(gè)例證 "從一點(diǎn)點(diǎn)開(kāi)始一個(gè)長(zhǎng)的方法"。 在先前的章節(jié)中我們提到一些將來(lái)工作的可能性，我們?cè)谶@里概述。 ? 引進(jìn)規(guī)那么的完全理論的議題應(yīng)該是被追求的，雖然這不可能有許多實(shí)際的影響。 ? 在證明搜尋期間，怎樣合并輔助定理的議題是應(yīng)該追求的?？死赘竦牟迦胙a(bǔ)助定理意味著以句法的特征為根底的新奇方式在當(dāng)前目標(biāo)和一個(gè)輔助定

64、理之間被分享：如果一個(gè)輔助定理和當(dāng)前目標(biāo)以不同的語(yǔ)言被表達(dá)，這時(shí)輔助定理為了要證明當(dāng)前目標(biāo)是沒(méi)有什么用的?？死赘竦牟迦胙a(bǔ)助定理為 FOL 支撐，但是把擴(kuò)充的主意到較富有的理論是有可能的。 ? 完成可能被擴(kuò)充為完全的完成la Huet。有條件的完成也應(yīng)該被實(shí)現(xiàn)，以便它應(yīng)付通常的情形，而且支持理論應(yīng)該被開(kāi)展。更遠(yuǎn)地說(shuō)，為了支持不同的等式概念，完成的執(zhí)行應(yīng)該被一個(gè)等式的概念參數(shù)化，這等式與HOL的嵌入的等式不同。一件額外的工作是整合好自動(dòng)的終止證明器，就像完成程序的 AProVE，所以使用者交互作用是最小化的。 ? 自動(dòng)化的連接應(yīng)該被擴(kuò)充，以便使用者不會(huì)因太多的信息而忙得不可開(kāi)交。 ? 自動(dòng)化

65、整體上而言為了提高策略的效率，需要再實(shí)現(xiàn)。 ? 我們企圖實(shí)行替代選擇的方法和證明的搜尋去處理經(jīng)由適宜的關(guān)閉和連接等式 這包括將來(lái)的工作的產(chǎn)生作為這個(gè)工作的直接結(jié)果。我們現(xiàn)在考慮其他沒(méi)有被防范的時(shí)機(jī)。 雖然我們相信我們的方式很大地解決了一個(gè)被給定的輔助定理的證明問(wèn)題，但是輔助定理和定義的選擇主要是一個(gè)技巧的事情。在輔助定理的情況下，我們典型地在理論的邊界上累積它們，然后尋找一般的輔助定理，它包含了幾個(gè)這樣的例子。這些增強(qiáng)是歸納假定的增強(qiáng)的回憶。 我們也發(fā)現(xiàn)在一些領(lǐng)域中,在理論之間有一個(gè)在邊界上的非瑣細(xì)的輔助定理的爆發(fā)，這在推廣上無(wú)法被減少。這典型地普通數(shù)學(xué)對(duì)象的發(fā)生，就像一棵樹(shù)。許多輔助

66、定理直觀上似乎合理的，但是它們的證明時(shí)常包括相當(dāng)多的努力。在這情況下，似乎很難控制子理論的傳播使其進(jìn)入主要的理論，因?yàn)樽永碚摰妮o助定理是如此的普遍被用于主要的理論之中。因此在這里我們有三個(gè)相關(guān)的問(wèn)題，即： ?來(lái)自一個(gè)子理論的重要而獨(dú)立的輔助定理的擴(kuò)展被請(qǐng)求。 ?輔助定理的直觀似乎合理的，這很難去證明。 ?輔助定理滲入主要理論,減少模組化和使主要的理論很重地依賴在子理論上。 這里似乎沒(méi)有方法減少在一些輔助定理里的爆發(fā)。根據(jù)證明，我們注意到困難從需要發(fā)生小心地說(shuō)歸納法補(bǔ)助定理，所以這主要地是歸納證明的一個(gè)自動(dòng)化的失敗。我們也注意在這一個(gè)區(qū)域中的大部份的定義暗示可運(yùn)行,以至于這里有一些模式檢查的形式范圍經(jīng)由定義的執(zhí)行。這依次能用來(lái)告誡一個(gè)歸納的證明器作為事實(shí)或不同的猜想輔助定理。 我們沒(méi)有提及自動(dòng)化的歸納法，或其他的更高階的功能。我們有更多要說(shuō)關(guān)于在章節(jié)？的介紹。但是能夠說(shuō)這可能像一個(gè)困難的領(lǐng)域。 我們也注意關(guān)于在策略混合的推論方面的困難。我們感覺(jué)到最近的提議朝向微積分學(xué)的策略可以證明是有趣的。我們建議相對(duì)瑣細(xì)的步驟, 就像確定策略手寫(xiě)體是樹(shù)結(jié)構(gòu)而不是線性的結(jié)構(gòu), 而且在證明