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

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

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