命题演算形式系统在Isabelle HOL中的形式化.ppt

1、伊莎贝尔/HOL命题演算形式化系统，王莉莉讲师：王园园教授，张兴元教授，第14届全国离散数学研讨会，主要内容，定理证明工具伊莎贝尔命题演算形式化系统PC完备性定理证明命题演算形式化系统ND概要，主要内容，定理证明工具伊莎贝尔命题演算形式化系统PC完备性定理证明命题演算形式化系统ND概要，定理证明工具伊莎贝尔， 交互式定理证明工具主要功能：描述和验证主要应用领域：数学定理证明和形式验证功能强大的灵活性丰富的符号表达能力Isar结构化证明风格自动生成类型化文档，主要内容，定理证明工具Isabelle命题演算形式系统PC完备性定理证明命题演算形式系统nd摘要，命题演算形式系统PC，理论部分系统中推理

2、命题公式的真值证明和演绎，基本上构成了PC的语言部分， 命题演算形式系统PC机，PC机的语言部分基本上构成了系统中推理命题公式的真值证明和演绎，以及基本组成。 PC机的语言部分通过归纳定义引入了三个构造函数Atom:Atom公式negimplicit，PC机中的公式由两个连词组成，PC机中公式的形式定义，类型atom=NAT数据类型exp=Atom | neg exp(！-200 200) |隐式exp exp (infixr181)，使用类型同义，原子公式的下标类型为自然数，优先级满足右组合，PC中公式的形式定义和基本构成，PC的公理系统，PC的理论部分，包括三种公理模式，可用Isabell

3、e/HOL的归纳定义公式集来描述。consts axm : exp集电感式axm内含A 1: A B A axm A 2:(A B C)(A B)A C axm A :(！a！B)A axm，命题演算形式系统PC，基本上构成PC语言部分的理论部分，系统中推理命题公式真值的证明和推导，系统中的推理，命题公式2.1真值的定义如果公式A包含命题自变量p1、p2、p3、pn，则表示为a (P1、p2、P3、pn)。任何给定的p1、p2、p3、pn的值条件称为赋值，a有一个确定的真值。当a在赋值时取真值，它被称为真a；在伊莎贝尔/HOL，赋值由函数env表示，公式的真值由返回真或假的函数trvalue给

4、出。公式的真值定义如下，定义采用原始递归。常量trvalue : exp(NAT bool)bool pri rec trvalue(Atom n)env=env n trvalue(！idspnexcel _ NV)。A) env=(tr值a env) tr值(a b) env=(tr值a env tr值b env)，系统内的推理，定义2.2公式A被称为永恒真理或同义反复，如果进行了任何赋值，它将为真。形式表达式是env。真。公式a叫做可满足性，如果有赋值，让a取值为真。它可以正式表示为env。真。否则，a被称为不满意，或永远虚假。系统中的推理，定义2.3表示公式a逻辑上隐含公式b，它被记录

5、为a b，并且如果a的所有赋值都被验证，则公式b也必须被验证。那就是：env。tr值a env=真tr值b env=真；类似地，公式集逻辑暗示公式b如下。(a.a tr值a env=真)tr值b env=真。在HOL，演绎的形式定义如下：常量c:exp集exp集演绎是一个从公式集到公式集的函数语法可推导3360:exp集exp pool(in xpc 51)判断一个给定的公式是否是一组前提公式的演绎结果，符号pc是将普通数学逻辑教科书中的定义与翻译pc a PC()归纳PC()内含PC a MP 3360pca统一起来用上面的形式定义，不难表示公式A是一个定理.如果公式a是前提，演绎结果可以表

6、示为axmpc a。到目前为止，命题演算形式系统pc的形式定义已经建立。基于这一定义，作者分析并验证了与个人计算机相关的性质和定理。，属性2.1个人电脑是单调的。也就是说，g1 g2 pc g1 pc g2也可以表示为g1 g2 pc (axmg1) pc (axmg2)。这不难用个人电脑的归纳定义来证明。定理2.1(演绎定理)的形式表达式是：axmpacb=axmpcab。在pc机上用归纳法证明了这种必要性。充分性证明使用分离规则将原始目标分解为两个子目标。两个方向的证明都使用了pc的定义和以前证明过的PC的单调性。属性2.2 A axm trvalue A env=真，也就是说，公理总是真

7、的。定理2.2(个人电脑是合理的)。(TR值B环境=真)TR值A环境=真定理2.3(个人计算机是一致的)(个人计算机是一致的！定理2.4(个人计算机不完整)答：个人计算机不完整！命题演算形式化系统pc完备性定理证明命题演算形式化系统ND摘要，完备性定理证明，讨论形式化系统PC的完备性是非常重要的，形式化命题演算形式化系统PC的完备性证明也是非常必要和困难的。采用的技术路线是：首先，用哥德尔编码将PC机中的公式用自然数编码，同时给出解码方案，并正式验证编码的正确性。参考文献5中关于完备性证明中特殊情况=的讨论扩展到一般情况，定理仍然成立。完备性定理的证明，特例=: env。一般情况：环境。(b.

8、b tr值b env=true) tr值a env=true axmpca，主要内容，Isabelle命题演算形式系统PC完备性定理的证明命题演算形式系统nd概要，为了描述方便，Isabelle/HOL在形式化ND系统时仍使用完全连词短语和，这并不影响讨论ND系统的推理和性质，但在推理规则中省略了6个与连词和和相关的推理规则，保留了其余8个。nd的形式定义，常量nd:3360 (exp set) exp)集合归纳ND内含子nd-axm:b(，b)ND hyp :(，b) nd (a，b)ND hyp :(a，b)ND；(！A，B) nd(，B) nd阻抗： (A，B) nd(，AB) nd阻抗：(A，d)；(，AB) nd(，B) nd负： (A，B)nd；(一，B) nd(，B) nd负：(，A)nd；(，a)nd；(，B)和dngI:(，A)和(，a)和dngE:(，要证明ND也是合理和完整的并不难。它们被正式表示为以下两个定理：定理4.1和环境。(b.b tr值b env=真)tr值a env=真定理4.2 env。综上所述，本文在伊莎贝尔/HOL建立了命题演算形式系统的逻辑模型，并从形式上验证了其正确性。具体来说，主要有以下几个方面：给出了概率中心的形式化定义，并对一些重要的性质和定理以及概率中心的合理性和完备性进行了形式化验证。证明了命