（计算机软件与理论专业论文）交互式并行定理证明环境的构建.pdf

兰越走学礤士学茳论文交互式并行定璎涯明环境熬梭建 原刨性声明 本人郑重声明：本人所呈交的学位论文，是在导师的指导下独立进行研究 所取褥的残象。擎娩论文中凡芎| 霜稳a 已经发表戴束发表酶或柒、数据、溪赢 等，筠跫麟确注翡毽殛。狳文中基经注鬻雩| 麓魏内容羚，不毯含殛薅其惫令入 或集体已经发表或撰写过的科研成果。对本文的研究成果做出羹骚贡献的个人 和集体，均已在支中激孵确方式标粥。 本声辅熬法律凌镁癞奉天零攫+ 论文作者签名：一 日期： 兰地大学碗士学位论文交互式并行定理证明环境的构建 关于学位论文使用授权的声明 本人在导师指导下所完成的论文及相关的职务作品，知识产权归属兰州大 学。本人完全了解兰州大学有关保存、使用学位论文的规定，同意学校保存或 向国家有关部门或机构送交论文的纸质版和电子版，允许论文被查阅和借阅； 本人授权兰州大学可以将本学位论文的全部或部分内容编入有关数据库进行检 索，可以采用任何复制手段保存和汇编本学位论文。本人离校后发表、使用学 位论文或与该论文直接相关的学术论文或成果时，第署名单位仍然为兰州大 学。 保密论文在解密后应遵守此规定。 论文作者签名： 导师签名：日期 2 兰妯大学硕士学毽论文 交互式并行定理证明环境的构建 摘要 机器定理证明在数学定理证明、协议验证、软件和硬件的形式化验证等方 面发挥出越来越重要的作用。为了提高定理证明器的工作效率和自动化程度， 人们开发了各种定理证明系统，主要有自动化和交互式两种类型。 i s a b e l l e 是种用来构造交互式定理证明器的逻辑框架，由它构造的 i s a b e l l e h o l 是一种功能完备的定理证明系统。在i s a b e l l e 中证明定理的主 要方法是策略，即完成一步或多步基本推理的程序。证明的过程是用户选择策 略，然后机器执行策略，如此反复直到完成证明。所以，在i s a b e l l e 中定理证 明的核心问题就是找到能够完成证明的一个策略序列。 本文设计并实现了一种以i s a b e l l e 为基础的并行定理证明环境，它通过在 多个运行i s a b e l l e 的服务器上同时执行各自的策略来实现对定理的并行证明。 然后以此为基础讨论几种并行证明策略及一种自动化证明策略。该自动化证明 策略的基本思想是对给定的策略集，系统以并行方式同时尝试由其中的策略组 成的各策略序列，从而实现自动定理证明的目的。 【关键词】机器定理证明并行自动定理证明i s a b e l l e 兰州7 笋黜；慧岔趁立 交互式并行定理证明环境的构建 a b s t r a c t i th a sb e c o m em o r ea n dm o r ei m p o r t a n tt h a tt h ea p p l i c a t i o no f t h e o r e mp r o v i n go l lm a t h e m a t i ct h e o r e mp r o v i n g ，p r o t o c o lv e r i f i c a t i o n h a r d w a r ev e r i f i c a t i o na n ds o f t w a r ev e r i f i c a t i o n i no r d e rt oi m p r o v e t h ee f f i c i e n c ya n dt h ea u t o m a t i o no ft h ep r o c e d u r ed u r i n gp r o v i n g ， v a r i o u sk i n d so ft h e o r e mp r o v e r sh a v eb e e nd e v e l o p e d ，f a l l i n gi n t o i n t e r a c t i v eo ra u t o m a t i cc a t e g o r i e s i s a b e l l ei sal o g i cf r a m e w o r ku s e dt oc o n s t r u c tt h e o r e mp r o v e r s i s a b e l i e h o l ，w h i c hc a m ef r o mi s a b e l l e ，i sat h e o r e mp r o v e rw i t b m a t u r ef u n c t i o n s t h em a i nm e t h o du s e di ni s a b e l l et op r o v et h e o r e m s i st a c t i c ，w h i c hi sap r o g r a ma c c o m p l i s h i n go n es t e po rm a n ys t e p s o fb a s i cd e d u c t i o n t h ep r o c e s so fc o n s t r u c t i n gap r o o fi st oc h o i c e at a c t i cb yt h eu s e ra n dt h e nt oe x e c u t et h et a c t i co nac o m p u t e r r e p e a t e d l yu n t i lt h ep r o o fi sc o m p l e t e s ot h em a i np r o b l e m i nt h e o r e m p r o v i n gi ni s a b e l l ei st of i n das e q u e n c eo ft a c t i c sw h i c hc a nb e u s e dt op r o v eat h e o r e m t h i sp a p e rd e s c r i b e sa ni m p l e m e n t a t i o no fac o n s t r u c t i o no fa p a r a l i e lt h e o r e mp r o v i n gs y s t e mb a s e do ni s a b e l l e i td i s t r i b u t e s t h ep r o v i n gt a s k st os o m es e r v e r sr u n n i n gi s a b e l l ei no r d e rt op r o v e t h e o r e m si np a r a l l e l a n dt h e nd i s c u s s e ss e v e r a la u t o m a t i ct a c t i c s b a s e do ni t t h em a i ni d e a so ft h et a c t i c si st h a t ，f o rag i v e ns e t o ft a c t i c s ，t h es y s t e mt r yt op r o v eat h e o r e mt h r o u g hc h e c k i n ga l l s e q u e n c e sc o m p o s e db yt h et a c t i c s i nt h es e ti no r d e rt op r o v e t h e o r e m sa u t o m a t i c a l l y k e y w o r d s ：t h e o r e mp r o v i n g ，p a r a l l e l ，a u t o m a t i ct h e o r e mp r o v i n g i s a b e ll e 4 兰钠大学碗士学位论文交互式并行定理证明环境的构建 第一章研究背景 本章简要介绍机器定理证明的发展概况、本文的目标、所采用的方案以及 目前完成的工作，最后是后续章节的介绍。 1 1 背景简介 随着计算机软硬件技术的发展，人们在工作和生活中越来越多地依赖于各 种计算机系统。为了有效地设计和实现这些系统并且确保系统功能的正确性， 人们开始利用各种形式化方法。机器定理证明就是其中的主要方法之一。 机器定理证明最早产生于莱布尼茨的设想，它是对“数学推理”的形式化， 是利用计算机来证明定理的软件系统。它一方面提供描述定理的形式语言，另 一方面又提供证明定理的推理工具，从而将一个包含公理、推理规则和定理的 推理系统抽象成一个符号系统，最终实现在系统内以机械化的方式来构造定理 的证明。如今人们不仅可以利用它证明许多数学领域的定理，而且开始把它应 用于协议验证、硬件验证和程序验证等新领域。这些领域中的证明任务若以手 工方式来做，一方面证明过程很容易出错，另一方面计算量太大，从而基本上 失去了证明的意义。虽然形式化方法也有它的局限性，哥德尔就曾经在他著名 的不完备性定理中指出不可判定性的存在，但形式化方法在工程实践中仍然是 一种非常有力的方法，在近几十年不断得到发展。 由于各种应用的不同需要，出现了多种逻辑系统，如一阶谓词逻辑、高阶 逻辑、时态逻辑等。为了在逻辑系统中有效地实现推理，出现了多种证明方法， 如自然推理、序列演算、归结原理、表演算等及其各种改进形式( 本节详细内 容见第二章) 。相应地也出现了多种多样的机器定理证明系统。从工作方式的不 同可以把它们分为自动化系统和交互式系统两大类。 机器定理证明技术的发展经历了从自动到交互，再回到自动的过程。人们 最早设计的定理证明系统是自动化的。随着应用的复杂化，如c p u 验证问题中 的大量公式，自动化定理证明系统受到了运行时间和空间上的挑战，于是出现 了交互式定理证明系统。 一个交互式定理证明系统需要在用户的帮助下来构造定理的证明。在证明 6 兰弛大学硕士学位论文 交互式并行定理证明环境的构建 定理的过程中，用户给出一条规则，然后机器就执行一步推理，如此反复。更 为复杂的交互方式则要求用户给出一个程序，定理证明系统通过执行程序完成 多个推理步骤。这个程序通常叫做策略( t a c t i c ) ，证明定理就是执行策略。当 然在执行策略时系统真正执行的还是建立在系统中的公理和推理规则。l c f 是 第一个基于策略的交互式定理证明器，现在大多数的交互式定理证明器都在使 用策略。 回到自动意味着提高效率，即更高的性能和更少的交互。为了提高效率， 人们采用了并行和集成等措施。 并行计算可用于各种对性能有很高要求的应用中，如人工智能、三维动画、 化学、生物学和物理学中的科学计算问题。如果没有并行计算技术，一些问题 的计算机求解可能会失去意义。现在，并行计算技术已开始应用于机器定理证 明领域，主要以小粒度、中粒度和大粒度三种方式应用于自动化定理证明系统 中，使其性能有了很大的提高。但在交互式定理证明系统中的应用还较为少见， 并且以小粒度和中粒度为主。 集成是指把各种方法集成到一起，从而增强系统的证明能力。如在交互式 定理证明系统中引入自动化证明策略，这些策略或者采用自动化证明技术实现， 或者把定理翻译到专门的自动化定理证明系统中，在后者完成证明后再把其证 明合并到前者中。这样既可以获得更高的性能，也可以把原来需要多次交互才 能完成的证明变为自动完成。 1 2 问题的提出 机器定理证明的核心问题是搜索问题，即花费最少的代价找到证明。有了 策略后，交互式定理证明的过程就是应用策略的过程，定理的证明本身就是一 个所用( 有效) 策略的序列，从而证明一个定理就是要找出那个策略序列。 给定一个定理t ，给定一个策略的集合s ，怎样从s 中找到一个策略序列p 正好构成t 的一个证明? 1 3 论文的主要工作 本文探讨在i s a b e l l e ( 一种交互式定理证明系统，详细内容见第二章) 中 兰州大学硕士学位论文交互式并行定理证明环境的构建 以并行的方式解决问题，即首先构造基于i s a b e l l e 的一个并行证明环境，然后 设计寻找p 的并行策略。本文主要完成了以下工作： ( 1 ) 构造基于i s a b e l l e 的并行定理证明环境； ( 2 ) 实现管理策略的小型语言； ( 3 ) 设计b l a s t 并行策略、o r 并行策略、并行证明策略和并行搜索策略 等四种并行定理证明策略。重点是其中的并行搜索策略，它用于实现证明过程 的自动化。 1 4 论文结构 后续章节的内容安排如下： 第二章机器定理证明简介：简要介绍机器定理证明的基本方法、i s a b e l l e 中的基本概念以及当前并行定理证明的各种形式。 第三章并行证明环境的建立：在分析各种常用并行结构的基础上，提出系 统的总体结构，并说明系统中各部分程序间数据通信的解决方案。 第四章并行算法的设计和实现：说明所设计的语言和4 种并行策略：( 1 ) b l a s t 并行策略：( 2 ) 并行证明策略；( 3 ) o r 并行策略；( 4 ) 并行搜索策略。 第五章将来的工作：提出进一步的工作目标。 兰她大学硕士学位论文交互式并行定理证明环境的构建 第二章机器定理证明简介 本章介绍机器定理证明的基本方法、并行定理证明的概况以及i s a b e l l e 的 基本概念。 2 1 定理证明的基本方法及搜索问题 一个形式系统i 由下列四个部分组成：( 1 ) 字母表a ，它是一个非空集合； ( 2 ) 公式集e ，它是一个由a 中的符号的有限序列构成的集合；( 3 ) 公理集a x ， 它是e 的一个子集；( 4 ) 规则集r ，它是e 上的部分运算构成的一个集合。l = 称为i 的形式语言。 称为i 的形式演算。 设s 是一个有限公式集。如果有限公式系列f 。，f 一，f 。满足：( 1 ) f 。是一 个公理；或者( 2 ) f 是s 中的一个公式；或者( 3 ) f 。能够由序列中它前面的 公式通过应用某个规则得到，这时公式系列f 。f 一，f 。就构成f ( = f n ) 的一个 证明。 由形式系统的定义我们看到它有如下两个特征：( 1 ) 抽象性。形式系统一 旦建立完成，便与一切实际意义毫不相关，我们只能在形式系统外赋予符号这 样或那样的含义。( 2 ) 机械化。形式系统中的推导是一个可机械实现的过程， 在形式系统中，公式、规则和证明等概念有十分严密和精确的定义，可以使未 受任何专i 1 i 7 1 1 练的人所掌握。 为了有效地进行推理，人们发现了多种形式演算的方法，如自然推理 ( n a t u r a ld e d u c t i o n ) 、序列演算( s e q u e n tc a l c u l u s ) 、归结原理( r e s o l u t i o n p r i n c i p l e ) 、表演算( t a b l e a u ) 等。下面分别用这些方法来证明定理： 如果a b ，并且b c ，那么a c 成立。 自然推理是从数学推理中抽象出来的。它的推理规则模仿了人们在日常生 活中的推理模式，因而较为直观。自然推理对于每个联结词都有引入规则和消 除规则，如图l 中的蕴涵引入规则( 一i ) 导致在结论中出现蕴含联结词，蕴含 消除规则( 一e ) 导致前提中的蕴涵联结词在结论中消失。规则中横线上面的是 前提，下面的是结论。对于蕴涵引入规则( 一i ) ，先假设r 成立，然后设法证 明s 成立，再运用该规则得到结论r s 。此后r 成立的假设就不能再使用了， q 兰铂大学硕士学位论文 交互式并行定理证明环境的构建 图中的方框就表示这些假设有效的范围。 图1 自然推理 r i 志( 叫 掣( 。) s 、7 序列演算与自然推理类似，但它采用逆向证明的方式，并把前提和结论分 别写在一的左侧和右侧。序列的基本形式为a 一，a 。一b 一，b 。，当a ， a 。蕴 含b v v b 。时序列为真。序列演算的推理规则分为左规则和右规则，分别相当 于自然推理中的消除规则和引入规则，并且都具有引入规则的性质，所以适用 于自动推理。 劢抽：f 堡兰丝 s g 辛日 ，兰：堡三丝：三 g j h s _ r 劢加：r 堡兰丝爿船 g t 丁，hj h ，丁 。，g ：丝! 兰! ! 垡：三里 s _ 丁，g ，g j h ，h 妨协：r 生主a劢加：f 坐主4 劢加：， 4 兰型 乃加：r 堡兰 。，苎：笪：皇：+ ，笪：妻4 ： ，三里：垒丝= 兰4 ：4 = b _ c a a _ c a s s - - - - - - - - - - - - - - - - 乃访：， 童 孤加，! 竺夏五，t h i n ：l 笪! g ! b 曼, 妻c 。c 二孤加：r 曼量堡 r 笪! 竺曼妻 _ + ，里兰旦：= 鱼旦兰= 曼 b - c b j a _ c ，墨= 里：型= 鱼生旦= 鱼星：型= 笪 4 一且b - - c 号a - c 图2 序列演算 归结原理又称消解原理，在机器定理证明和人工智能中有非常广泛的应用。 兰抽大学硕士学位论文 交互式并行定理证明环境的构建 归结原理采用反证法。它先把公式的否定形式化为主合取范式，得到一个子句 集。公式的不可满足性就等价于该子旬集的不可满足性，而子句集的不可满足 性又取决于是否能归结得到空子句。由于没有公理并且只有唯一的推理规则， 所以归结原理非常适合于自动化推理。 ，( ( a _ b ) ( b + c ) _ ( a _ c ) ) ( a b ) ( b c ) ，( a c ) ) ( ，a v b ) ( - b v c ) a 、c a k ”c ) 型需 蚀 ， 川6 b ，b 图3 归结原理 表演算和归结原理类似也是一种反证法。其推理过程是构造一颗二叉树。 如果从根结点到叶结点的路径中包含一个公式及其否定的话，该结点就处于关 闭状态( a o s e d ) ，标记为“+ ”号，并在后续的推理中不再生长。如果在整棵 树停止生长时所有的叶结点都是关闭的，就得到了矛盾的结论。表演算也适合 于构造自动证明。 a b ( 1 ) j b c ( 2 ) 1 ( a c )( 3 ) 1a ( 4 f r o m l ) b ( 5 f r o m l ) 入 ： 1 b ( 6 f r o m2 ) c ( 7 f r o m2 ) 1b ( 8 f r o m 2 ) c ( 9 f r o m2 ) a ( 1 0 f r o m3 )a ( 1 1 f r o m3 )+ ( 5a n d8 ) i 1c ( 1 3 f r o m3 ) 1 c ( 1 4 f r o m3 ) i + ( 4a n d1 0 )+ ( 4a n d1 1 ) 图4 表演算 一个机器定理证明系统是实现一个形式系统的计算机软件，它由两部分组 门 ， 兰一 岬1 吖i 忡 兰纳- 欠学硕士学位论文 交互式并行定理证明环境的构建 成：( 1 ) 描述定理的形式语言；( 2 ) 证明定理的推理工具。 针对不同的应用领域，运用不同的形式演算方法，出现了多种机器定理证 明系统，主要分为交互式定理证明器( i n t e r a c t i v et h e o r e mp r o v e r ) 和自动 化定理证明器( a u t o m a t i ct h e o r e mp r o v e r ) 两大类。 交互式定理证明器以人机交互为基础。在证明定理的过程中，用户先指定 每一个证明步骤要做的工作，然后由计算机完成具体的工作细节。部分交互式 定理证明器可能带有一个逻辑框架( 1 0 9 i c a lf r a m e w o r k ) ，从而具有很强的表 达能力，可用于实现非常复杂的形式系统，如i s a b e l l 。交互式定理证明器 往往基于有类型的l a m b d a 演算( t y p e dl a m b d a c a l c u l u s ) 及自然推理，常用 的有用于验证硬件和实时系统的h o l 0 1 和p v s 。1 ，用于数学形式化的c o q 。1 等。 自动化定理证明则较少需要用户的直接干预，它们应用各种专门的算法、 数据结构和优化技术，自动确定每一个推理步骤的工作，具有极高的推理速度， 能够证明一些非常复杂的问题。现在己开发出很多高性能的自动化定理证明器， 如v a m p i r e “、o t t e r ”1 、s e t h e o “1 以及p t t p 旧等。自动化定理证明系统一般限 于带等式的一阶谓词逻辑，并且大都依赖于归结原理。 在定理证明系统中证明定理的证明过程既可以看作是一个状态序列，也可 以看作是一个改变状态的规则序列。当然，对于不同的形式演算方法，状态和 规则是不同的，如表演算中的状态是树的各个生长阶段，归结原理中的状态指 不断改变的子句集合，而在自然推理中状态则是需要证明的各个子目标等。至 于推理规则的差异则更为明显。 定理证明中的一个重要问题是搜索问题( s e a r c h p r o b l e m ) 。对于给定的证 明系统i ，一组前提h 和一个有待证明的公式p ，我们希望从h 出发在i 中构造 出p 的一个证明，或者从h u 一p ) 出发推导出一个矛盾。搜索问题就是在构造 证明或矛盾的过程中可以利用的各种控制措旌，使得只使用尽可能少的资源就 能完成证明。 搜索问题的核心是证明计划。证明计划包括三个部分：( 1 ) 一个规则选 择函数，它根据当前的证明状态选择下一步要使用的证明规则f ：( 2 ) 一个前 提选择函数，它选择将要传递给f 的一组前提；( 3 ) 一个判断函数，它根据当 前的证明状态判断证明是否成功。不同种类的定理证明器其实就是以不同的方 式处理证明过程中的证明计划。 兰娟大学硕士学位论文 交互式并行定理证明环境的构建 2 2 并行定理证明概况 并行计算技术是一种提高定理证明效率的有力方法。根据并行操作粒度的 不同，机器定理证明中的并行分三个级别，分别是小粒度、中粒度和大粒度。 小粒度和中粒度的并行不改变证明计划，而大粒度的并行则可能改变证明计划。 小粒度的并行作用在公式中项的级别上，其并行操作发生在推理步骤内部， 是推理步骤内部的并行，如项匹配( t e r m m a t c h i n g ) 、项合一( t e r mu n i f i c a t i o n ) 以及项重写( t e r mr e w r i t i n g ) 等。由于在推理过程中这些低级别的操作出现 的频率很高，如果能通过并行来加快它们的执行速度的话，就能够提高整个推 理过程的执行效率。 中粒度的并行作用在公式的级别上，它是推理步骤之间的并行。如并行归 结( p a r a l l e lr e s o l u t i o n ) 。中粒度并行的意义在于通过同时执行多个推理步 骤来加快定理证明执行的速度。 大粒度的并行作用在证明计划的级别上，主要有两种基本方式。一种方式 是分布式搜索( d i s t r i b u t e ds e a r c h ) 。它先对问题进行分解得到不同的搜索范 围，并行进程对各自的搜索范围执行相同的搜索计划。由于各进程仅搜索问题 空间的一部分，所以进程间的并行能有效地提高系统的性能。另一种方式是多 重搜索( m u l t i s e a r c h ) 。这时各进程对整个问题执行不同的搜索计划，每个进 程有可能得到由别的进程传递过来而按照它本身的搜索计划在以后才能产生的 那些数据，对这些数据的利用有可能提高推理执行的效率。当然这里的划分并 不十分严格，一个实际的证明过程有可能同时包含多重搜索和分布式搜索两个 方面的特性。 在并行系统中不仅有推理控制的任务，而且还包括并行控制的任务。在推 理控制和并行控制相分离的情况下，系统成为主从结构( m a s t e ra n ds l a v e ) 。 主端负责通信控制和任务划分，从端负责完成推理任务，如p s a t o ”3 。在推理控 制和并行控制相结合的情况下，这时每一个进程都有自己的证明计划，系统成 为对等结构( p e e r ) 。 虽然从理论上来说，共享内存和分布式内存的并行系统都能实现各种类型 的并行，但实际上小粒度和中粒度的并行适合于在共享内存的并行计算机上实 现，而大粒度的并行则适合于在网络或计算机机群的环境中运行。 兰柚大学硕学位论文 交互式并行定理证明环境的构建 并行计算在自动化定理证明器中的应用较多。研究表明，并行能够有效地 提高自动化定理证明器的速度，如o t t e r “1 和r 0 0 。”的并行版本在很多基准测 试中都表现出明显的加速效果，s e t h e o 的并行版本也有类似的表现。 但是在交互式定理证明器中，并行技术的应用却相对较少。究其原因大致 是并行对系统的基本要求是自动化，交互式的工作方式经常需要用户的参与， 而用户是难以同时面对多个计算单元的。 自从l c f 在交互式定理证明器中引进策略( t a c t i c s ) 以来，现今的大多数 交互式定理证明器都开始使用策略。所以在交互方式下，小粒度的并行就是策 略内的并行，中粒度或大粒度的并行就是策略间的并行。 对于策略内的并行，每当用户要求计算机执行一个策略时，通过并行可以 在更短的时间内完成任务，但人机交互并没有减少，只是计算机工作的时间更 短而已。采用这种方法的有n u p r l 的并行版本。 策略问的并行往往通过异类系统间的集成表现出来，如交互式定理证明器 和自动化定理证明器之间的集成。剑桥大学计算机实验室正在进行的一个项目 就是把i s a b e l l e z f 和v a m p i r e ( v a m p i r e 近年来在自动定理证明领域一直处于 领先地位，它在c o n f e r e n c eo na u t o m a t e dd e d u c t i o n 组织的相关大赛中屡屡 获奖) 集成起来“。它把i s a b e l l e z f 的部分证明任务交给v a m p i r e 去完成， 等v a m p i r e 完成任务后，再把v a m p i r e 的证明合并到i s a b e l l e z f 的证明中。 这样，不仅充分利用了v a m p i r e 的高性能和高速度，而且对某些原本需要多个 策略才能完成的证明任务，现在利用v a m p i r e 能够直接完成。所以这种方法不 仅能够提高速度而且能够减少交互，是一种不错的选择。 a h r e n d t 曾把k i v 和基于表演算的定理证明器3 t a p 集成起来“，但结果并 不令人满意，其中的部分原因可能是3 t a p 没有v a m p i r e 那么优秀的表现。较为 成功的是j o h nh a r r i s o n 针对h o ls y s t e m 所作的工作“。他把自己的自动定 理证明器与h o l 集成起来，在h o l 中建立了名为m e s o n t a c 的工具，该工具成 为h o l 中最强有力的工具之一。j o eh u r d 也曾把g a n d a l f 与h o ls y s t e m 集成 起来，实现了从g a n d a l f 的证明到h o ls y s t e m 的证明的翻译“。 在实际完成证明之前，用户并不知道应该使用哪些策略，所以用户需要尝 试，这正是交互式定理证明的交互性的表现。用户可以输入一个策略，然后观 察策略执行的结果，据此判断是否应该换用另外一个策略，再开始新的尝试， 1 4 兰伯太学碗士学位论文交互式并行定理证明环境的构建 如此往复。 能否让能让用户一次同时尝试多个策略? 如果并行执行这些策略就可以使 用户等待少量策略的执行时间却尝试了更多的策略，甚至完成整个证明，这是 本文方案的基本出发点。 2 3i s a b e l l e 简介 i s a b e l l e 是剑桥大学计算机实验室开发的一种用于构造形式系统的通用工 具。它通过提供一个用来描述形式系统的逻辑框架，使用户能够在i s a b e l l e 中 构造出自己的形式系统，然后在自己系统中以交互方式完成各项推理任务。 i s a b e l l e 自身的逻辑系统是它的元逻辑，用户在i s a b e l l e 中构造出来的 形式系统是它的对象逻辑。用户既可以从头( i s a b e l l e p u r e ) 开始构造自己的 系统，也可以从已有的对象逻辑( 如i s a b e l l e h o l ) 中派生出自己的系统来。 在随i s a b e l l e 发布的软件包中已有f o l ( f i r s to r d e rl o g i c ) 、z f ( z e r m e l o f r a e n k e ls e tt h e o r y ) 、h o l ( h i g h e ro r d e rl o g i c ) 、l c f ( t h el o g i c f o rc o m p u t a b l ef u n c t i o n s ) 等多种对象逻辑系统。其中最为完善、应用也最 为普遍的是h o l ，也就是高阶逻辑。用户往往在由i s a b e l l e h o l 派生出的系统 中工作，并且可以使用i s a b e l l e 为各种对象逻辑系统提供的大量工具，如自动 化证明工具等。 定理证明 对象逻辑 浯法 策略 j 元逻辑 j 图5i s a b e l l e 的系统结构 i s a b e l l e 是一个运行在l i n u x 操作系统中的集成环境，整个系统由m l 语 言解释程序、i s a b e l l e 、i s a r 及用户界面( p r o o fg e n e r a l ) 等几个部分组成， 如图5 所示。在i s a b e l l e 发行包的s r c 子目录中有i s a b e l l e i s a r 本身及h o l 等对象逻辑的完整源代码，还包括在i s a b e l l e 中完成的大量的定理证明。 兰炳又学硕士学位论文交互式并行定理证明环境的构建 用户在i s a b e l l e 中的工作有两种类型： ( 1 ) 在i s a b e l l e 的元逻辑中构造对象逻辑( 定义状态) ： ( 2 ) 在i s a b e l l e 的对象逻辑中证明定理( 证明状态) 。 i s a b e l l e 的元逻辑是一种最小化的高阶逻辑，它带有联结词八( 全称量词) 、 = = ( 蕴含) 、；( 等于) ，并根据推理规则来实现推理，这也是交互式定理证明 器常用的推理方式。在表达推理规则或待证明的定理时使用宽括号组织前 提，用长箭头= = 把前提和结论分开。例如，合取引入规则： ! ( c o pa q 可表示为： p ：o = = p a q 。如果不使用宽括号的话，合取引入规则也 可表示为：p = = ( q 一 p a q ) 。 在i s a b e l l e 中定义对象逻辑时，用户需要做两个方面的工作：( 1 ) 描述对 象逻辑的语法规则和推理规则：( 2 ) 通过运用内建在i s a b e l l e 中的推理机制构 造应用于对象逻辑的策略。结合这两方面的工作，用户就可以得到一个自己的 逻辑系统。 i s a b e l l e 把用户要求证明的公式t 表示为定理( t h e o r e m ) 或引理( 1 e m m a ) 。 在给出定理( 引理) 后，i s a b e l l e 就进入证明状态，并把需要证明的定理作为 目标( g o a l ) 看待：盯= = t 。证明的过程就是运用策略把规则作用于目标， 从而得到更加简单当然也可能是更多个数的子目标：i t 。：t ：t 。= = t ， 直到i 3 = 0 ，即没有目标为止，这时就完成了一个证明。由此也可以看出i s a b e l l e 用同样的格式表示推理规则和证明状态。 策略是运用推理规则改变目标的程序。i s a b e l l e 中的策略有三种：( 1 ) i s a b e l l e 自身的策略，用户可以直接使用；( 2 ) 用户自行开发的策略；( 3 ) 组 合策略，它把已有策略组合到一起成为新的策略。在i s a b e l l e 中开发策略并不 容易，它需要用户对i s a b e l l e 中的内部数据类型( 如公式、项和数据类型在 m l 语言中的定义) 有深入的了解，并且要深入分析i s a b e l l e 源代码中的大量 函数( 1 0 万行规模) 。好在用户一般不需要编写自己的策略。 应用策略时，其结果有可能成功也有可能失败。应用策略成功意味着目标 发生变化或者消失，应用策略失败则不改变当前的证明目标。由此可以看出定 理证明的关键就在于对策略的选择，而由用户自己做出选择的证明方式正体现 了交互式定理证明的特征。所以在i s a b e l l e 中的定理证明就是一个策略序列， 1 6 兰蚰大学硕学位论文交互式并行定理证明环境的构建 每次对策略的成功应用就形成证明过程中的一个证明步骤。 i s a b e l l e 支持两种风格的证明，一种是策略风格的证明，另一种是描述风 格的证明。在策略风格的证明中，只说明所用的策略，而没有说明运用策略后 变化了的目标。这种风格有利于证明的构造，这是因为在i s a b e l l e 的集成环境 中随时可以看到当前的证明状态( 即目标) 。但在单独面对证明，也就是不在计 算机上运行的时候，用户是很难想象出每个证明步骤所对应的子目标的。所 以这种风格的证明不利于交流。描述风格的证明对每个证明步骤既说明所用 的策略又描述当前的目标，它出现在i s a r 中，它也是i s a b e l l e 近年来取得的 最大进展之一。 用户在i s a b e l l e 中的工作实际上是一种函数式程序设计，具体包括个三部 分的代码：( 1 ) i s a b e l l e 定义代码，主要实现对象逻辑中的数据类型、函数、 语法和推理规则等的定义；( 2 ) m l 程序代码，主要实现对象逻辑中的证明策略； ( 3 ) i s a b e l l e 证明代码，即对象逻辑中的定理证明。由于i s a b e l l e 是用m l 语言实现的，所以i s a b e l l e 代码与m l 语言的编程风格有些相似。 下面通过一个例子来说明i s a b e ll e 的基本原理、功能和应用。该例以f o l ( f i r s to r d e rl o g i c ) 为基础，模拟了p r o l o g 语言中对表这种数据结构的处 理，包括表的拼接和颠倒表中元素的次序。关于如何在m l 语言中开发策略程序 的问题需要较大的篇幅且不是本文的目标，所以这个例子中没有定义专门的策 略。 h e a d e r 术f i r s t o r d e rl o g i c ：p r o l o ge x a m p l e s ) t h e o r yp r o l o g i m p o r t sf o l b e g i n t y p e d e c l al i s t a r i t i e s1 i s t ：( ”t e r m ”) ”t e r m ” c o n s t s n “：al i s t ” c o n s ：” a ，al i s t = al i s t ”( i n f i x r ”：”6 0 ) a p p ：” al i s t ，al i s t ，al i s t = 0 ” r e v ：” al i s t ，al i s t = 0 ” 1 7 兰挑大学硕士学位论文 交互式并行定理证明环境的构建 a p p n i l ：”a p p a p p c o n s ：”a p p r e v n i l ： ”r e v r e v c o n s ：1 i ( x ：x s ，z s ) ” e n d r e v n i l x s ，y s ，z s ) = = a p p ( x ：x s ，y s ，x ：z s ) ” n i l ，n i l ) ” ( x s ，y s ) ：a p p ( y s ，x ：n i l ，z s ) | = = r e v 用户构造的对象逻辑表现为i s a b e l l e 中的理论( t h e o r y ) 。t h e o r yp r o l o g 定义了名为p r o l o g 的理论。i m p o r t sf o l 表明p r o l o g 理论将建立在f o l 对象 逻辑的基础之上。理论的主体内容在随后的b e g i n 和e n d 之间。 t y p e d e e l al i s t 是对数据类型的说明。a 是一个类型变量，al i s t 则 定义了一个由a 类型的元素组成的“表”数据类型，它的数据在后面的c o n s t s 中定义。虽然没有指定a 的具体类型，由于可以指定a 类型的变量，这对于本 例已经足够了。 a r i t i e s 是对l i s t 的进一步说明。第一个t e r m 表明l i s t 中的元素是项 ( t e r m ，一阶谓词逻辑中的基本概念) 类别( s o r t ) 的数据，它规定了a 这个 类型变量只能是项类别中的类型。第二个t e r m 表明1 i s t 本身也是项。 c o n s t s 用于定义常量或函数：n i l 、c o n s 、a p p 和r e v 。 ( 1 ) n i l 表示空表，它是我们构造除空表外更多表类型数据的起点。 ( 2 ) c o e s 表示单个元素和表的拼接函数，其结果还是一个表。它用于实 现从n i l 出发构造出更多的表。定义： c o n s ：” a ，al i s t = al i s t ”( i n f i x r ”：”6 0 ) 由名称、类型和简称三个部分组成。第一部分c o n s 是函数名。第二部分” a ，a l i s t = al i s t ”表示函数的数据类型，它起到c 语言中函数原型的作用。类 型中的短箭头“= ”表明这是一个函数类型。箭头左边方括号中是函数的两个 参数的类型，箭头右边是函数结果的类型。这种只有一个箭头的类型定义的是 c 语言风格的普通函数。如果把类型表示为”a = al i s t = al i s t ”的形 式，所定义的函数就成为克里函数( c u r r yf u n c t i o n ) 。克里函数是一种高阶函 数，对f ：”a = al i s t = al i s t ”而言，其特别之处在于如果调用时 只给定一个参数，如fx ，就得到了另一个也只需要一个参数的新函数。新函 兰能大学硕士学缱论文交互式并行定理证明环境的构建 数要求的参数就是原来f 的第二个参数。克里函数是函数型程序设计中特有的 现象，有点像泛函分析中的泛函，我们无法在c 语言中做到这一点。定义中的 第三个部分( i n f i x r ”：”6 0 ) 定义了函数的简称，用冒号“：”表示。i n f i x r 表 示用中缀格式使用冒号，最后个字母r 表示右结合性质( 从而a ：b ：c ：n i l 被 理解为a ：( b ：( c ：n i l ) ) ) ，6 0 是运算的优先级。使用简称可以把构造新表的操作 c o n s ( x ，x s ) 表示为更加直观的x ：x s 。 ( 3 ) a p p 表示两个表的合并，其结果还是一个表。在a p p 后面的o 类型是 f o l 中的逻辑类型。没有把a p p 表示为”a1 i s t = al i s t = a1 i s t ”的 类型源自于p r o l o g 语言的特性。在p r o l o g 语言中表的合并可用谓词a p p e n d 表 示为： a p p e n d ( ，l ，l ) a p p e n d ( hj t l ，l i s t 2 ， h t 3 ) ：一a p p e n d ( t 1 ，l i s t 2 ，t 3 ) 这两个语句的含义是：空表和l 表结果的合并为l 表；如果t 1 和l i s t 2 合 并得到t 3 ，那么 h l t l 和l i s t 2 合并得到 h l t 3 。在 h l t 3 中h 是表头元素， t 3 是表尾，它也是一个表。由于a p p e n d 是谓词，它不是直接作用于两个表得 到第三个表，而是对三个表之间是否成立合并关系做出判断，体现了函数与谓 词之间的差异：前者有明确的输入输出关系，而后者没有。 ( 4 ) r e v 表示表的反转。和a p p 一样，它不是直接运算出结果而是判断两 个表的反转关系是否成立。在p r o l o g 语言中表的反转用谓词r e v e r s e 表示为： r e v e r s e ：一( ， ) r e v e r s e ( h l t ，l ) ：一r e v e r s e ( t ，m ) ，a p p e n d ( m ， h ，l ) 这里的做法是把一个表的表头h 追加到该表表尾的反序表上达到表反序的 目的。 a x i o m s 部分定义的是公理或推理规则。没有长箭头的是公理，如”a p p ( n i l ， y s ，y s ) ”。有长箭头的是推理规则，如”a p p ( x s ，y s ，z s ) = = a p p ( x ：x s ，y s ，x ：z s ) ”。 箭