基于高階邏輯的定理證明方法及其對策的應用

康 漫 張 杰 李曉娟 關 永

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

基于高階邏輯的定理證明方法及其對策的應用

康 漫1張 杰1李曉娟2關 永2

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

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

定理證明方法 形式化驗證 定理證明器 證明方法 對策

0 引 言

形式化方法是保證計算機系統設計正確性的一條重要途徑。它是用數學的方法表達設計的系統的實現及其規范或性質，根據數學理論來證明所設計的系統實現滿足其規范或性質。

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

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

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

1 證明方法與對策

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

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

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

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

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

2 支持高級證明步驟及其對策的應用

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

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

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

作者在大量的實踐中發現，利用高級證明步驟中的對策進行證明，最常用的就是Cases_on和Induct_on這兩個對策，使用這兩個對策有兩個關鍵所在：一是如何選擇恰當的對策。對策選擇的恰當與否直接影響到后續證明步驟的繁瑣與簡單，甚至影響證明的結果。二是如何選擇這些對策作用的參數。參數選取的合適，將會簡化證明步驟，如果選擇的不合適將有可能影響證明結果。

下面圍繞這兩個典型的對策進行詳細的分析和描述，并給出它們在應用過程中可能出現的問題和解決方法。

(1) Cases_on對策

Cases_on是最常用的一種證明對策，其類型為term -> tactic[6]，所以在應用該對策時要提供一個項作為參數。該對策基于項的類型ty，使用TypeBase數據庫中類型ty的情況定理，對證明目標進行情況分解。

通常情況下，Cases_on的參數可以是變量。對于一個既定的證明目標，如果對目標不能再進行化簡，HOL4理論庫中已經存在的定理能夠對情況分解之后的子目標進行證明，可以使用該對策完成目標的情況分解。

例如現有一個證明目標：“對于任意的兩個自然數m與n，如果m整除n，那么m≤n，或者n=0”。系統要想對其進行形式化證明，HOL4系統中已存在divides的定義divides_def ： `a dividesb=?x.b=a*x`，所以可以考慮使用重寫對策進行化簡?；喌玫降淖幽繕酥泻许?(m*x)，而在HOL4系統中不存在關于這種形式的項的可用的定理，已存在定理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)形式的項，所以，我們可以對x施加情況分解對策Cases_on，得到的子目標的基本項與定理MULT_CLAUSES中項的形式相同，我們可以使用重寫對策進行下一步的證明[7]。如圖2所示。

圖2 Cases_on對策參數為變量的例子

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

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

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

圖3 Cases_on對策參數為非變量的例子

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

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

(2) Induct_on對策

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

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

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

圖4 使用對策Induct_on的例子

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

圖5 使用對策Cases_on的例子

支持高級證明步驟能夠從證明目標的變量或項中，返回其類型定義時存儲的定理，從而減輕用戶證明的負擔。支持高級證明步驟中的對策除了可以返回情況定理和歸納定理，還可以返回重寫規則，這時還需要用戶考慮使用type_rws對策，這里不再做詳細介紹。

3 自動推理

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

PROVE_TAC對策的類型是：thm list -> tactic[9]，所以在應用該對策時要提供一個定理表作為參數。該定理表中包含推導目標所需的公理、定義及定理，系統將根據假設和提供的定理使用一階推理推導證明目標。

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

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

圖6 使用對策PROVE_TAC的例子執行

PROVE_TAC對策的結果只有兩種情況，證明成功或者證明失敗。當系統根據已有的假設和給定的定理或公理進行推導，超出系統設置的搜索深度時，仍沒有證明目標，則應用該對策失敗。PROVE_TAC對策定理表的構建可以參考已有文獻[10]。其實自動推理還包含其他的對策，比如:METIS_TAC能夠自動實例化存在量詞，DECIDE_TAC對策可以對線性代數的證明應用一個決策程序，這里不再做詳細介紹。

4 化簡器及其重寫對策的應用

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

SRW_TAC與RW_TAC類似，是一種功能很強大的重寫對策，其類型為ssfrag list -> thm list -> tactic[6]。該對策是對一個潛在的化簡集工作，通過函數srw_ss進入該化簡集，可以添加“化簡集片段”和定理而增大化簡集?；喖且粋€特定的集合，其中包含了一些特定領域的重寫定理。在系統中存儲許多類型的情況下，RW_TAC的功能就足夠了，這是因為在證明目標之前，它可以為已知的類型重復地添加所有的重寫定理到一個化簡集當中。但是SRW_TAC只需要加載一次重寫到srw_ss()下的化簡集，在這種情況下，SRW_TAC速度更快。

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

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

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

圖7 使用對策SRW_TAC的例子

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

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

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

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

圖8 使用對策STRIP_ASSUME_TAC的例子

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

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

圖9 使用對策by的例子

化簡器中的重寫對策主要的功能是對目標進行化簡，當化簡的目標與系統中已存在的定理一樣時，重寫對策也可以直接證明目標。重寫對策定理表的構建可以參考已有文獻[10]。HOL4系統中還有更多的重寫對策，如REWRITE_TAC, ASM_REWRITE_TAC和ONCE_ASM_REWRITE_TAC等，關于它們的使用可以參考重寫對策的應用的文獻[10]?；喥髦羞€存在一類以SIMP_CONV轉換為中心的化簡對策，有興趣的讀者可以自行查閱。

5 結 語

HOL4系統中提供了數百個對策及幾千個定理，對于HOL4的使用者來說，選擇合適的對策證明目標，不是一件容易的事情。本文通過討論支持高級證明步驟、自動推理和化簡器的三種證明方法，以及分析三種證明方法相對應的對策的功能、應用環境和應用中可能出現的問題，以期對HOL4系統用戶進行定理證明提供有效的幫助和啟發。另外，在HOL4系統中進行形式化驗證的方法有很多，本文提出的方法是用戶最易接受和使用的方法，并從理論上給出了一個完整的證明框架。因此，本文提供的證明思想和方法，對其他的基于高階邏輯的定理證明器(例如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] 錢振江,黃皓,宋方敏.操作系統形式化設計與安全需求的一致性驗證研究[J].計算機學報,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] 張杰,毛丹雯,關永,等.重寫對策在基于HOL的形式化證明中的應用[J].計算機工程與設計,2013,34(10):3664-3668.

[11] 韓俊剛,杜慧敏.數字硬件的形式化驗證[M].北京:北京大學出版社,2001:3-9.

[12] 李兵.交互式并行定理證明環境的構建[D].甘肅省蘭州市:蘭州大學,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。國家自然科學基金項目(61572331,61373034)?？德T士生，主研領域：形式化驗證。張杰，副教授。李曉娟，教授。關永，教授。

TP301.2

A

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