交互式并行定理證明環(huán)境的構建.pdf

1、機器定理證明在數(shù)學定理證明、協(xié)議驗證、軟件和硬件的形式化驗證等方面發(fā)揮出越來越重要的作用。為了提高定理證明器的工作效率和自動化程度，人們開發(fā)了各種定理證明系統(tǒng)，主要有自動化和交互式兩種類型。 Isabelle是一種用來構造交互式定理證明器的邏輯框架，由它構造的Isabelle/HOL是一種功能完備的定理證明系統(tǒng)。在Isabelle中證明定理的主要方法是策略，即完成一步或多步基本推理的程序。證明的過程是用戶選擇策略，然后機器執(zhí)行策

2、略，如此反復直到完成證明。所以，在Isabelle中定理證明的核心問題就是找到能夠完成證明的一個策略序列。 本文設計并實現(xiàn)了一種以Isabelle為基礎的并行定理證明環(huán)境，它通過在多個運行Isabelle的服務器上同時執(zhí)行各自的策略來實現(xiàn)對定理的并行證明。然后以此為基礎討論幾種并行證明策略及一種自動化證明策略。該自動化證明策略的基本思想是對給定的策略集，系統(tǒng)以并行方式同時嘗試由其中的策略組成的各策略序列，從而實現(xiàn)自動定理證明的目