康 漫 張 杰 李曉娟 關(guān) 永

1(北京化工大學(xué)信息科學(xué)與技術(shù)學(xué)院 北京 100029) 2(首都師范大學(xué)信息工程學(xué)院 北京 100048)

基于高階邏輯的定理證明方法及其對策的應(yīng)用

康 漫1張 杰1李曉娟2關(guān) 永2

1(北京化工大學(xué)信息科學(xué)與技術(shù)學(xué)院 北京 100029)2(首都師范大學(xué)信息工程學(xué)院 北京 100048)

定理證明是形式化驗(yàn)證的主要方法之一，其中定理證明器的使用是難點(diǎn)。為了提高證明效率，論述HOL4系統(tǒng)中主要的三種證明方法：支持高級證明步驟。自動推理和化簡器，為定理的證明提供了一個完整而通用的理論框架。詳細(xì)說明了以上三種證明方法的相關(guān)對策的功能和應(yīng)用環(huán)境，并為應(yīng)用中可能出現(xiàn)的問題提出解決方案。給出的對策應(yīng)用實(shí)例不僅體現(xiàn)了三種方法中相關(guān)對策的實(shí)用性，還進(jìn)一步表明了提出解決方案的有效性。

定理證明方法 形式化驗(yàn)證 定理證明器 證明方法 對策

0 引 言

形式化方法是保證計(jì)算機(jī)系統(tǒng)設(shè)計(jì)正確性的一條重要途徑。它是用數(shù)學(xué)的方法表達(dá)設(shè)計(jì)的系統(tǒng)的實(shí)現(xiàn)及其規(guī)范或性質(zhì)，根據(jù)數(shù)學(xué)理論來證明所設(shè)計(jì)的系統(tǒng)實(shí)現(xiàn)滿足其規(guī)范或性質(zhì)。

形式化驗(yàn)證主要包括等價(jià)性檢驗(yàn)、模型檢測和定理證明。這三種方法各有優(yōu)缺點(diǎn)。等價(jià)性檢驗(yàn)主要是檢驗(yàn)設(shè)計(jì)變換前后的一致性，但是不能進(jìn)行規(guī)范和性質(zhì)的驗(yàn)證。模型檢測的優(yōu)點(diǎn)是完全自動化，如果系統(tǒng)不滿足給定的性質(zhì)，檢驗(yàn)結(jié)果可以給出反例，但是模型檢測存在狀態(tài)組合爆炸問題。定理證明的方法是用某種邏輯的形式化系統(tǒng)的公式表示所驗(yàn)證的系統(tǒng)及其性質(zhì)，以該形式化系統(tǒng)的公理和推理規(guī)則為基礎(chǔ)，可以逐步推導(dǎo)出表達(dá)系統(tǒng)性質(zhì)的公式。定理證明能夠處理無限狀態(tài)的系統(tǒng)，但是這種驗(yàn)證方法的代價(jià)較高，需要較高的數(shù)學(xué)能力并要經(jīng)過相當(dāng)時(shí)間的訓(xùn)練。因此，定理證明器的使用對定理證明方法的應(yīng)用和發(fā)展起著至關(guān)重要的作用。

Higher Order Logic(HOL) 系統(tǒng)是最成熟的用于驗(yàn)證的定理證明器之一。它是由英國劍橋大學(xué)的M.J.C.Gordon教授等在80年代開發(fā)的一種形式化驗(yàn)證系統(tǒng)，其最新的版本為HOL4。近年來，它已被廣泛應(yīng)用于數(shù)學(xué)定理的證明、軟件驗(yàn)證、協(xié)議驗(yàn)證和程序驗(yàn)證[1-4]。

關(guān)于定理證明器HOL4系統(tǒng)的理論和對策，有相關(guān)的文獻(xiàn)介紹[5-8]，但是這些文獻(xiàn)的介紹只適合于用于理解HOL4系統(tǒng)，并不能為用戶提供證明的思路。Slind等對HOL4系統(tǒng)的邏輯，理論和對策等進(jìn)行了總的概述。作者在文中指出了用HOL4進(jìn)行證明的通用的方法：支持高級證明的步驟、化簡器和一階搜索[9]，但是作者并沒有進(jìn)行進(jìn)一步的闡述和說明。文獻(xiàn)[10]對Slind等指出的化簡器中重寫對策的應(yīng)用進(jìn)行了詳細(xì)的說明，但是并沒有完成HOL4系統(tǒng)常用證明方法的闡述。為了能更好更快地完成定理的證明，本文提供了通用的，完整的證明方法，說明了其相關(guān)對策的功能和使用環(huán)境，并對其應(yīng)用中出現(xiàn)的問題提出了解決方案。通過給出的常用對策的應(yīng)用實(shí)例，不僅體現(xiàn)了三種方法的實(shí)用性，而且進(jìn)一步表明了提出解決方案的有效性。

1 證明方法與對策

HOL4系統(tǒng)是一種交互式定理證明系統(tǒng)。所謂交互式定理證明系統(tǒng)，是指在高層由人做引導(dǎo)工作，在底層由機(jī)器自動化地處理一部分定理推導(dǎo)與證明問題[9]。在HOL4系統(tǒng)中完成定理證明的基本方法有兩種，即正向證明法和目標(biāo)制導(dǎo)法。正向證明方法是從要證明定理的假設(shè)條件出發(fā)，利用系統(tǒng)中的公理、定理和推理規(guī)則等逐步推導(dǎo)出欲證定理。目標(biāo)制導(dǎo)證明法首先假設(shè)欲證明的定理為真，并將其作為初始目標(biāo)，再通過使用對策引導(dǎo)系統(tǒng)根據(jù)已知條件、公理、定義和定理產(chǎn)生簡化的子目標(biāo)。反復(fù)使用對策對子目標(biāo)進(jìn)行不斷地化簡，直到當(dāng)前子目標(biāo)可以利用某個對策直接證明為止[11]。由于正向證明方法不能快速而有效地完成證明，所以在HOL4系統(tǒng)中，通常使用的證明方法是目標(biāo)制導(dǎo)法。

目標(biāo)制導(dǎo)法當(dāng)中，仍然需要人工的選擇相應(yīng)的證明對策，在HOL4系統(tǒng)中有大量的對策，在這個擁有龐大數(shù)量對策的系統(tǒng)中，如何快速準(zhǔn)確地找到合適的對策，是用戶完成證明的關(guān)鍵[12]，也是證明的難點(diǎn)。如果用戶采用熟悉大量的對策，然后再選擇對策進(jìn)行證明的方法，將會浪費(fèi)大量的時(shí)間和精力。這種證明途徑是不科學(xué)的、盲目的。為此本文給出的高效可行的證明途徑是先確定證明方法，然后選擇其對應(yīng)的對策完成證明。HOL4系統(tǒng)中證明的方法有高級證明、簡化器、一階證明等。經(jīng)過作者的大量實(shí)踐，針對目標(biāo)制導(dǎo)法，本文指出HOL4中的高級證明和簡化器是非常有效的證明方法。

由于高級證明包括支持高級證明的步驟和自動推理，所以支持高級證明的步驟、自動推理和簡化器是本文介紹的三種證明方法。此三種證明方法從理論上為定理的證明提供了一個完整的框架。此理論框架如圖1所示。

在該理論框架中，對于任何需要證明的初始目標(biāo)，支持高級證明的步驟能夠利用HOL4的潛在功能搜索目標(biāo)中變量在定義數(shù)據(jù)類型時(shí)已經(jīng)證明的定理或規(guī)則，供用戶使用，大大減輕了用戶證明的負(fù)擔(dān)。其中使用支持高級證明步驟中的歸納方法證明遞歸法定義的數(shù)據(jù)類型、函數(shù)和謂詞是非常有效的。因?yàn)樵诤瘮?shù)性語言中程序的重復(fù)都是使用遞歸方法來完成，所以歸納法對于定理證明尤為重要。通過一次或多次使用支持高級證明的步驟得到的子目標(biāo)是初始目標(biāo)分解之后的結(jié)果，此時(shí)的子目標(biāo)的形式非常接近系統(tǒng)中已有的理論，便可以采用自動推理和簡化器進(jìn)行證明。自動推理可以用來證明演繹推理中已知條件、公理、定義和定理與證明目標(biāo)之間的蘊(yùn)含關(guān)系。自動推理是HOL4系統(tǒng)中必不可少的一種方法，它可以完成多次蘊(yùn)含關(guān)系的證明，這是其他對策所不具備的。簡化器用來證明演繹推理中已知條件、公理、定義和定理與證明目標(biāo)之間的等價(jià)關(guān)系。簡化器是HOL4系統(tǒng)中是極為重要的一種證明方法，這是因?yàn)槟繕?biāo)制導(dǎo)法的證明思想與簡化器的證明思路是一致的，都是利用已知條件和系統(tǒng)中已有的公理、定義、定理等完成證明目標(biāo)的化簡與證明。

該理論框架為定理的證明提供了一個通用的方法，也為用戶完成證明提供了基本的證明思路，提高了證明效率。然而證明方法的應(yīng)用離不開對策。HOL4系統(tǒng)中的對策是ML函數(shù)，主要實(shí)現(xiàn)以下三種功能：一是將要證明的目標(biāo)分解為子目標(biāo)，二是將要證明的目標(biāo)進(jìn)行化簡，三是對當(dāng)前目標(biāo)進(jìn)行證明。下面圍繞本文提出的理論框架中的三種證明方法及其相應(yīng)的對策進(jìn)行詳細(xì)的說明和分析。

2 支持高級證明步驟及其對策的應(yīng)用

HOL4中證明的觀點(diǎn)是由用戶在高層指導(dǎo)，自動推理完成輔助證明。因此，HOL4系統(tǒng)提供了一個類型索引定理的數(shù)據(jù)庫(包含情況分析、歸納等)，結(jié)合一些陳述證明結(jié)構(gòu)，用戶在高層可以執(zhí)行很多證明[9]。HOL4系統(tǒng)為用戶提供了許多支持高級證明步驟的對策，比如Induct、Cases、Cases_on、Induct_on等，這些對策都可以使用數(shù)據(jù)庫中的信息減輕HOL的應(yīng)用負(fù)擔(dān)[5]。

當(dāng)一個數(shù)據(jù)類型被成功定義的時(shí)候，關(guān)于這個新類型的一些標(biāo)準(zhǔn)定理被自動證明，并被添加到一個數(shù)據(jù)庫TypeBase中。這些支持高級證明步驟的對策有一個共同的特點(diǎn)，它們都可以在數(shù)據(jù)庫TypeBase中搜索數(shù)據(jù)類型，如果搜索到相應(yīng)的數(shù)據(jù)類型，就會返回這個類型已有的重寫規(guī)則，以及相關(guān)事實(shí)定理。用戶通過返回的定理進(jìn)行情況分析或者歸納，支持下一步的證明。在一些情況下，該類對策的使用將直接決定著證明的成功與失敗。

支持高級證明步驟的對策中有一類很重要的對策——?dú)w納對策，它可以有效地處理遞歸定義的數(shù)據(jù)型和函數(shù)。HOL4系統(tǒng)的元語言是ML語言，ML語言是函數(shù)性語言，函數(shù)性語言程序的重復(fù)主要靠函數(shù)的遞歸[11]，在這種情況下使用歸納法進(jìn)行證明就方便很多。因此，歸納證明方法在HOL4證明系統(tǒng)中是非常重要的一種證明方法。HOL4系統(tǒng)提供了幾種使用歸納法進(jìn)行證明的途徑，對于自然數(shù)和表等這些系統(tǒng)內(nèi)部理論，具有專用的對策進(jìn)行歸納[11]，而Induct_on對策是歸納證明中最常用的對策，它可以完成自然數(shù)和表的專用歸納對策的功能。

作者在大量的實(shí)踐中發(fā)現(xiàn)，利用高級證明步驟中的對策進(jìn)行證明，最常用的就是Cases_on和Induct_on這兩個對策，使用這兩個對策有兩個關(guān)鍵所在：一是如何選擇恰當(dāng)?shù)膶Σ?。對策選擇的恰當(dāng)與否直接影響到后續(xù)證明步驟的繁瑣與簡單，甚至影響證明的結(jié)果。二是如何選擇這些對策作用的參數(shù)。參數(shù)選取的合適，將會簡化證明步驟，如果選擇的不合適將有可能影響證明結(jié)果。

下面圍繞這兩個典型的對策進(jìn)行詳細(xì)的分析和描述，并給出它們在應(yīng)用過程中可能出現(xiàn)的問題和解決方法。

(1) Cases_on對策

Cases_on是最常用的一種證明對策，其類型為term -> tactic[6]，所以在應(yīng)用該對策時(shí)要提供一個項(xiàng)作為參數(shù)。該對策基于項(xiàng)的類型ty，使用TypeBase數(shù)據(jù)庫中類型ty的情況定理，對證明目標(biāo)進(jìn)行情況分解。

通常情況下，Cases_on的參數(shù)可以是變量。對于一個既定的證明目標(biāo)，如果對目標(biāo)不能再進(jìn)行化簡，HOL4理論庫中已經(jīng)存在的定理能夠?qū)η闆r分解之后的子目標(biāo)進(jìn)行證明，可以使用該對策完成目標(biāo)的情況分解。

例如現(xiàn)有一個證明目標(biāo)：“對于任意的兩個自然數(shù)m與n，如果m整除n，那么m≤n，或者n=0”。系統(tǒng)要想對其進(jìn)行形式化證明，HOL4系統(tǒng)中已存在divides的定義divides_def ： `a dividesb=?x.b=a*x`，所以可以考慮使用重寫對策進(jìn)行化簡。化簡得到的子目標(biāo)中含有項(xiàng) (m*x)，而在HOL4系統(tǒng)中不存在關(guān)于這種形式的項(xiàng)的可用的定理，已存在定理MULT_CLAUSES:|-!m n.(0*m=0)∧(m*0=0)∧(1*m=m)∧(m*1=m)∧(SUCm*n=m*n+n)∧(m*SUCn=m+m*n): thm，定理中含有(m*0)和(m*SUCn)形式的項(xiàng)，所以，我們可以對x施加情況分解對策Cases_on，得到的子目標(biāo)的基本項(xiàng)與定理MULT_CLAUSES中項(xiàng)的形式相同，我們可以使用重寫對策進(jìn)行下一步的證明[7]。如圖2所示。

圖2 Cases_on對策參數(shù)為變量的例子

由此可見，使用Cases_on對策對證明目標(biāo)進(jìn)行情況分解，系統(tǒng)會根據(jù)要分解變量的數(shù)據(jù)類型，將目標(biāo)分解為兩個子目標(biāo)，以便使用系統(tǒng)中已存在的定理進(jìn)行自動證明。因此使用該對策要求用戶對證明目標(biāo)中含有的變量的數(shù)據(jù)類型非常了解。

Cases_on的參數(shù)也可以是非變量，對于要證明的目標(biāo)，如果需要分情況討論才能證明，則也可以通過使用Cases_on對策對目標(biāo)進(jìn)行分情況證明。用項(xiàng)來表示非變量的參數(shù)，該對策可以將目標(biāo)分解為項(xiàng)成立和否定項(xiàng)的情況。通常情況下，目標(biāo)在不同情況下，使用不同的定理完成證明，用戶使用該對策分情況分解目標(biāo)。

例如現(xiàn)有一個證明目標(biāo):“對任意的一個表l，取表l的前m個元素再取前n個元素得到的表，與取表l的前MIN(m,n)個元素得到的表一樣”。在HOL4系統(tǒng)中已存在的定理LENGTH_TAKE: |- !n l. n <= LENGTH l ==> (LENGTH (TAKE n l) = n) : thm和TAKE_LENGTH_TOO_LONG:|- !l n. LENGTH l <= n ==> (TAKE n l = l) : thm，從這兩個定理中可以看出，需要將目標(biāo)分成`n <= LENGTH l`和`LENGTH l <= n`兩種情況證明，此時(shí)可以使用Cases_on對策，將目標(biāo)分成兩種情況的子目標(biāo)，然后使用已有的定理證明目標(biāo)。如圖3所示。

圖3 Cases_on對策參數(shù)為非變量的例子

由此可見，使用Cases_on對策對證明目標(biāo)進(jìn)行情況分解，系統(tǒng)根據(jù)項(xiàng)`m<=LENGTH l`，將目標(biāo)分解為`m<=LENGTH l`和`～(m<=LENGTH l)`兩種情況下的子目標(biāo)。這樣，用戶可以利用系統(tǒng)中已有的定理完成證明。

然而，當(dāng)定義的數(shù)據(jù)類型在Typebase中沒有情況定理時(shí)，使用Caese_on會失敗，也就是說并不適用于所有情況。如果庫中現(xiàn)有的定理不能完成證明，使用Caese_on不僅不能有效地支持證明，還會浪費(fèi)很多時(shí)間。因此，使用該對策用戶還需要對HOL4中的理論庫有一定的了解。

(2) Induct_on對策

Induct_on對策也是支持高級證明步驟中最常用的對策之一，它的類型是term -> tactic[6]，所以在應(yīng)用該對策時(shí)要提供一個項(xiàng)作為參數(shù)。該對策是基于項(xiàng)的類型ty，使用TypeBase數(shù)據(jù)庫中類型ty的歸納定理進(jìn)行歸納證明。

通常情況下，Induct_on的參數(shù)可以是變量也可以是非變量，對于一個既定的證明目標(biāo)，如果不能再對目標(biāo)進(jìn)行簡化，可以依據(jù)目標(biāo)存在的數(shù)據(jù)類型定義時(shí)的歸納定理進(jìn)行歸納證明。

如果證明的目標(biāo)為“對任意的一個表l，表l的長度小于等于n，那么取表l的前n個元素得到的是表l本身”。由于HOL4系統(tǒng)中表是遞歸定義的，對于表的定義及相關(guān)定理通常將表表示為[]或(h::t)的形式，所以對當(dāng)前目標(biāo)不存在已有的定理可以將其直接化簡。在HOL4系統(tǒng)中已存在的定義: TAKE_def: |- (!n. TAKE n [] = []) / !n x xs. TAKE n (x::xs) = if n = 0 then [] else x::TAKE (n - 1) xs : thm。此時(shí)可以使用Induct_on對策，將目標(biāo)中的表l分解成[]和(h::t)形式的子目標(biāo)。對于表為[]的子目標(biāo)，可以使用重寫對策直接證明。對于表為(h::t)的子目標(biāo)，可以使用重寫對策將其化簡，證明目標(biāo)。如圖4所示。

圖4 使用對策Induct_on的例子

多數(shù)情況下，對于相同的目標(biāo)，如果將Cases_on對策和Induct_on對策同時(shí)作用于這個目標(biāo)，且對策的參數(shù)相同，這時(shí)產(chǎn)生的子目標(biāo)個數(shù)是一樣的，如使用Induct_on對策的圖4和使用Cases_on對策的圖5的兩個例子所示。在使用Induct_on對策的圖4中產(chǎn)生的第2個子目標(biāo)中假設(shè)條件表中會存一個假設(shè)，這將使證明目標(biāo)的速度快于使用Cases_on對策的情況。

圖5 使用對策Cases_on的例子

支持高級證明步驟能夠從證明目標(biāo)的變量或項(xiàng)中，返回其類型定義時(shí)存儲的定理，從而減輕用戶證明的負(fù)擔(dān)。支持高級證明步驟中的對策除了可以返回情況定理和歸納定理，還可以返回重寫規(guī)則，這時(shí)還需要用戶考慮使用type_rws對策，這里不再做詳細(xì)介紹。

3 自動推理

高級證明中除了支持高級證明步驟，還有一種必不可少的證明方法——自動推理。當(dāng)假設(shè)條件，公理，定義和定理與證明目標(biāo)存在蘊(yùn)含關(guān)系時(shí)，使用自動推理中的對策非常有效，另外自動推理還能夠很好地處理多層蘊(yùn)含關(guān)系。下面介紹自動推理中最常用的對策PROVE_TAC對策。

PROVE_TAC對策的類型是：thm list -> tactic[9]，所以在應(yīng)用該對策時(shí)要提供一個定理表作為參數(shù)。該定理表中包含推導(dǎo)目標(biāo)所需的公理、定義及定理，系統(tǒng)將根據(jù)假設(shè)和提供的定理使用一階推理推導(dǎo)證明目標(biāo)。

通常情況下，對于一個既定的證明目標(biāo)，若已有的假設(shè)條件和定理能夠推導(dǎo)出目標(biāo)，則可以通過使用PROVE_TAC對策證明目標(biāo)。

如果存在圖6中的目標(biāo)” TAKE n l = TAKE m l”，從假設(shè)條件”n <= m”和” ～(n < m) ”，我們可以使用HOL4理論庫中已經(jīng)存在的定理NOT_LESS: [] |- !m n. ～(m < n) <=> n <= m : thm和LESS_EQUAL_ANTISYM: [] |- !n m. n <= m∧m <= n ==> (n = m) : thm，推導(dǎo)出”m=n”。此時(shí)，使用PROVE_TAC對策可以推導(dǎo)出”m=n”，從而，證明目標(biāo)。

圖6 使用對策PROVE_TAC的例子執(zhí)行

PROVE_TAC對策的結(jié)果只有兩種情況，證明成功或者證明失敗。當(dāng)系統(tǒng)根據(jù)已有的假設(shè)和給定的定理或公理進(jìn)行推導(dǎo)，超出系統(tǒng)設(shè)置的搜索深度時(shí)，仍沒有證明目標(biāo)，則應(yīng)用該對策失敗。PROVE_TAC對策定理表的構(gòu)建可以參考已有文獻(xiàn)[10]。其實(shí)自動推理還包含其他的對策，比如:METIS_TAC能夠自動實(shí)例化存在量詞，DECIDE_TAC對策可以對線性代數(shù)的證明應(yīng)用一個決策程序，這里不再做詳細(xì)介紹。

4 化簡器及其重寫對策的應(yīng)用

化簡器的一般作用是通過替換來化簡目標(biāo)，就是將目標(biāo)等式左邊的項(xiàng)與使用的定理的左邊的項(xiàng)相匹配，然后用定理等式右邊的項(xiàng)替換目標(biāo)等式右邊的項(xiàng)，從而化簡目標(biāo)。重寫對策在HOL4中就屬于化簡器一類。重寫是化簡對策中的核心操作，在HOL4中是極為重要的一類對策。重寫對策可以利用對策中指定的定理重寫證明目標(biāo)，即將HOL4系統(tǒng)中已有的公理、定義和定理與目標(biāo)中的表達(dá)式匹配，如果表達(dá)式與等式左邊式子的模式相同，則用等式右邊的式子替換該表達(dá)式，從而對證明目標(biāo)進(jìn)行化簡或證明[10]。下面介紹使用重寫對策的原則、使用問題及解決方法。

SRW_TAC與RW_TAC類似，是一種功能很強(qiáng)大的重寫對策，其類型為ssfrag list -> thm list -> tactic[6]。該對策是對一個潛在的化簡集工作，通過函數(shù)srw_ss進(jìn)入該化簡集，可以添加“化簡集片段”和定理而增大化簡集。化簡集是一個特定的集合，其中包含了一些特定領(lǐng)域的重寫定理。在系統(tǒng)中存儲許多類型的情況下，RW_TAC的功能就足夠了，這是因?yàn)樵谧C明目標(biāo)之前，它可以為已知的類型重復(fù)地添加所有的重寫定理到一個化簡集當(dāng)中。但是SRW_TAC只需要加載一次重寫到srw_ss()下的化簡集，在這種情況下，SRW_TAC速度更快。

SRW_TAC對策可以根據(jù)潛在的化簡集以及給定的化簡集片段和給定的公理、定義、定理等對證明目標(biāo)及假設(shè)條件表進(jìn)行重寫，且能自動處理證明目標(biāo)結(jié)論中的全稱量詞、合取符、析取符、蘊(yùn)含符，甚至是假設(shè)條件表中的存在量詞等。另外該對策還具備自動執(zhí)行案例分解、決策程序等更加高級的功能。

通常情況下，SRW_TAC功能強(qiáng)大，利用它可以快速完成許多證明目標(biāo)的化簡或證明工作。

如圖7中，目標(biāo)為“!h n. LENGTH (h::l) <= n ==> (TAKE n (h::l) = h::l)”，使用重寫對策便可將目標(biāo)化簡為假設(shè)條件表和定理中已成立的情況，完成對目標(biāo)的證明。

圖7 使用對策SRW_TAC的例子

重寫對策雖然能夠化簡目標(biāo)，但作者在實(shí)踐過程中發(fā)現(xiàn)，重寫對策在帶有條件的重寫中很容易失效。HOL4系統(tǒng)本身能夠進(jìn)行條件重寫，當(dāng)遇到帶有條件的定理時(shí)，化簡器會泄放假設(shè)條件，并將條件假設(shè)為真，然后再進(jìn)行目標(biāo)的重寫。盡管條件重寫功能很強(qiáng)大，但并不適合于所有的帶有條件的定理。在HOL4系統(tǒng)中只有少數(shù)通用的條件可以直接使用條件重寫，比如除數(shù)不能為0。但是對于大多數(shù)用戶定義的條件，HOL4系統(tǒng)中的重寫對策便不能處理。在這種情況下，如果還需要繼續(xù)使用重寫規(guī)則，則需要補(bǔ)充假設(shè)條件表，這樣才可以完成證明。

通常情況下，當(dāng)要補(bǔ)充的假設(shè)條件存在于HOL4已證明的定理中，可以將已證明的定理直接添加到假設(shè)條件表，這時(shí)候使用STRIP_ASSUME_TAC對策；當(dāng)補(bǔ)充的假設(shè)條件不存在于HOL4已證明的定理中，我們可以使用by對策。

STRIP_ASSUME_TAC的類型是thm_tactic[6]，該對策將一個定理分解為一個定理表，并添加它們到假設(shè)條件。

如對于圖8中的證明目標(biāo):“取一個表l的前m個元素，得到一個新表，再取新表的前n個元素，與取表l的前(MIN n m)個元素得到的表一樣”，已經(jīng)存在兩個假設(shè)條件` m <= LENGTH l ` 和 `～(n <= m)`，為了后面證明的需要，我們需要添加定理LENGTH_TAKE: |-!n l. n <= LENGTH l ==> (LENGTH (TAKE n l) = n) : thm，此時(shí)可以直接使用STRIP_ASSUME_TAC對策添加。

圖8 使用對策STRIP_ASSUME_TAC的例子

by的類型是term quotation * tactic -> tactic[6]，該對策有兩個參數(shù)，一個是項(xiàng)，表示在假設(shè)條件表中要添加的定理，一個是對策，該對策用來證明添加的定理是正確的。by對策的功能是證明一個定理，并將其添加到目標(biāo)的假設(shè)條件列表。

對于圖9中的例子，證明的目標(biāo)是“TAKE n (TAKE m l) = TAKE (MIN n m) l”，從假設(shè)條件表我們可以推導(dǎo)出” (LENGTH(TAKE m l))<=n”，將” (LENGTH(TAKE m l))<=n”添加到假設(shè)條件表，有助于我們使用HOL4理論庫中已有的定理證明目標(biāo)。但是如何將” (LENGTH(TAKE m l))<=n”添加到假設(shè)條件列表，我們可以使用by對策。這時(shí)將” (LENGTH(TAKE m l))<=n”設(shè)為by的第一個參數(shù)，作為要添加的假設(shè)，使用對策PROVE_TAC和定理LENGTH_TAKE:[] |- !n l. n <= LENGTH l ==> (LENGTH (TAKE n l) = n) : thm來證明要添加的假設(shè)。添加完假設(shè)條件，使用重寫對策，即可證明目標(biāo)。

圖9 使用對策by的例子

化簡器中的重寫對策主要的功能是對目標(biāo)進(jìn)行化簡，當(dāng)化簡的目標(biāo)與系統(tǒng)中已存在的定理一樣時(shí)，重寫對策也可以直接證明目標(biāo)。重寫對策定理表的構(gòu)建可以參考已有文獻(xiàn)[10]。HOL4系統(tǒng)中還有更多的重寫對策，如REWRITE_TAC, ASM_REWRITE_TAC和ONCE_ASM_REWRITE_TAC等，關(guān)于它們的使用可以參考重寫對策的應(yīng)用的文獻(xiàn)[10]?；喥髦羞€存在一類以SIMP_CONV轉(zhuǎn)換為中心的化簡對策，有興趣的讀者可以自行查閱。

5 結(jié) 語

HOL4系統(tǒng)中提供了數(shù)百個對策及幾千個定理，對于HOL4的使用者來說，選擇合適的對策證明目標(biāo)，不是一件容易的事情。本文通過討論支持高級證明步驟、自動推理和化簡器的三種證明方法，以及分析三種證明方法相對應(yīng)的對策的功能、應(yīng)用環(huán)境和應(yīng)用中可能出現(xiàn)的問題，以期對HOL4系統(tǒng)用戶進(jìn)行定理證明提供有效的幫助和啟發(fā)。另外，在HOL4系統(tǒng)中進(jìn)行形式化驗(yàn)證的方法有很多，本文提出的方法是用戶最易接受和使用的方法，并從理論上給出了一個完整的證明框架。因此，本文提供的證明思想和方法，對其他的基于高階邏輯的定理證明器(例如HOL light、PVS等)同樣適用。

[1] Zhang J,Mao D W,Guan Y.Formalization of linear space theory in the higher-order logic proving system[J].Journal of Applied Mathematics,2013,2013(1):66-71.

[2] 錢振江,黃皓,宋方敏.操作系統(tǒng)形式化設(shè)計(jì)與安全需求的一致性驗(yàn)證研究[J].計(jì)算機(jī)學(xué)報(bào),2014,37(5):1083-1099.

[3] Basin D,Capkun S,Schaller P,et al.Formal Reasoning about Physical Properties of Security Protocols[J].Acm Transactions on Information & System Security,2011,14(2):1-28.

[4] Wang A,Fei H,Gu M,et al.Verifying Java Programs By Theorem Prover HOL[C]//International Computer Software & Applications Conference.IEEE Computer Society,2006:139-142.

[5] Cambridge Research Center of SRI International.The HOL system DESCRIPTION(For HOL Kananaskis-10)[EB/OL].[2014-11-10].http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananask-10-description.pdf/download.

[6] Cambridge Research Center of SRI International.The HOL system REFERENCE(For HOL Kananskis-10)[EB/OL].[2014-11-10].http://sourceforge. net/projects/hol/files/hol/kananaskis-10/kananaskis-10-reference.pdf/download.

[7] Cambridge Research Center of SRI International.The HOL system TUTORIAL(For HOL Kananaskis-10)[EB/OL].[2014-11-10].http://sourceforge. net/projects/hol/files/hol/kananaskis-10/ kananask is-10-tutorial.pdf/download.

[8] Cambridge Research Center of SRI International.The HOL system LOGIC(For HOL Kananaskis-10)[EB/OL].[2014-11-10].http://sourceforge. net/projects/hol/files/hol/kananaskis-10/ kananask is-10-logic.pdf/download.

[9] Slind K,Norrish M.A Brief Overview of HOL4[C]//Theorem Proving in Higher Order Logics,International Conference,Tphols 2008,Montreal,Canada, August 18-21,2008.Proceedings.DBLP,2008:28-32.

[10] 張杰,毛丹雯,關(guān)永,等.重寫對策在基于HOL的形式化證明中的應(yīng)用[J].計(jì)算機(jī)工程與設(shè)計(jì),2013,34(10):3664-3668.

[11] 韓俊剛,杜慧敏.數(shù)字硬件的形式化驗(yàn)證[M].北京:北京大學(xué)出版社,2001:3-9.

[12] 李兵.交互式并行定理證明環(huán)境的構(gòu)建[D].甘肅省蘭州市:蘭州大學(xué),2006:1-54.

THEOREMPROVINGMETHODBASEDONHIGHERORDERLOGICANDITSAPPLICATION

Kang Man1Zhang Jie1Li Xiaojuan2Guan Yong2

1(CollegeofInformationScienceandTechnology,BeijingUniversityofChemicalTechnology,Beijing100029,China)2(CollegeofInformationEngineering,CapitalNormalUniversity,Beijing100048,China)

The use of theorem proving system is always a difficult point in theorem proving method, and the theorem proving is one of the main methods of formal verification. In order to improve the efficiency of proof, three main methods of proof in HOL4 system are discussed: support for high-level proof steps, automated reasoning and simplification. This paper provided a complete and general theoretical framework for proving theorems. The function and application environment of the commonly used tactics in above methods were analyzed in detail. We proposed solutions to the problems in applications. The application of the proposed strategy not only reflects the practicability of the relative measures in the three methods, but also shows the effectiveness of the proposed solution.

Theorem proving method Formal verification Theorem proving system Proof method Strategy

2017-01-16。國家自然科學(xué)基金項(xiàng)目(61572331,61373034)?？德?，碩士生，主研領(lǐng)域：形式化驗(yàn)證。張杰，副教授。李曉娟，教授。關(guān)永，教授。

TP301.2

A

10.3969/j.issn.1000-386x.2017.11.002