《命题演算形式系统在isabellehol中的形式化》由会员分享，可在线阅读，更多相关《命题演算形式系统在isabellehol中的形式化（35页珍藏版）》请在金锄头文库上搜索。
1、命题演算形式系统在命题演算形式系统在 Isabelle/HOLIsabelle/HOL中的形式化中的形式化 王 俐 莉 指导教师：王元元教授 张兴元教授 全国离散数学第14届研讨会 主要内容主要内容 定理证明工具Isabelle 命题演算形式系统PC 完备性定理的证明 命题演算形式系统ND 总结 主要内容主要内容 定理证明工具Isabelle 命题演算形式系统PC 完备性定理的证明 命题演算形式系统ND 总结 定理证明工具定理证明工具IsabelleIsabelle 交互式定理证明工具 主要功能：描述和验证 主要应用领域：数学定理证明和形式化验证 特点 很强的灵活性 丰富的符号表达能力 Isa
2、r结构化的证明风格 自动产生排版好的文档 主要内容主要内容 定理证明工具Isabelle 命题演算形式系统PC 完备性定理的证明 命题演算形式系统ND 总结 命题演算形式系统命题演算形式系统PCPC 基本构成 PC的语言部分 PC的理论部分 系统内的推理 命题公式的真值 证明和演绎 命题演算形式系统命题演算形式系统PCPC 基本构成 PC的语言部分 PC的理论部分 系统内的推理 命题公式的真值 证明和演绎 基本构成基本构成 PC的语言部分 采用归纳定义 引入了三个构造子 Atom ：原子公式 Neg Imply PCPC中公式的形式化定义中公式的形式化定义 types atom = nat d
3、atatype exp = Atom atom | Neg exp (!- 200 200) | Imply exp exp (infixr 181) 使用了类型同义，原子公式的下标 类型为自然数 优先级 满足右结合 PCPC中公式的形式化定义中公式的形式化定义 基本构成基本构成 PC的理论部分 PC的公理系统包括三个公理模式，在Isabelle/HOL中可采用归纳定 义的公式集合来刻画。 consts axm : exp set inductive axm intros a1: A B A axm a2: (A B C) (A B) A C axm a3: (!A !B) B A axm 命
4、题演算形式系统命题演算形式系统PCPC 基本构成 PC的语言部分 PC的理论部分 系统内的推理 命题公式的真值 证明和演绎 系统内的推理系统内的推理 命题公式的真值 定义2.1 如果公式A含有命题变元p1, p2, p3, , pn， 记为A(p1, p2, p3, , pn)。对任意给定的p1, p2, p3, , pn的一种取值状况，称为指派（assignment）， A均有一个确定的真值。当A在指派下取值真时，称 弄真A；反之称弄假A。 系统内的推理系统内的推理 在Isabelle/HOL中，指派用函数env来表示，公式的真 值由函数trvalue给出，它返回True或False。下面给
5、出 PC中公式真值的定义，定义采用原始递归。 consts trvalue : exp (nat bool) bool primrec trvalue (Atom n) env = env n trvalue (! A) env = ( trvalue A env) trvalue (A B) env = ( trvalue A env trvalue B env) 系统内的推理系统内的推理 定义2.2 公式A称为永真式或重言式（tautologies ），如果对任意指派，均弄真A。形式化表示为： env. trvalue A env = True。公式A称为可满足 的（satisfactab
6、le），如果存在指派使A在下取 值真。可形式化表示为： env. trvalue A env = True。否则称A为不可满足的（unsatisfactable） ，或永假式。 系统内的推理系统内的推理 定义2.3 称公式A逻辑蕴含（logic imply）公式B， 记为AB，如果所有弄真A的指派亦必弄真公式B。 即： env. trvalue A env = True trvalue B env = True； 类似的，公式集逻辑蕴含公式B可如下表示： env. ( A. A trvalue A env = True) trvalue B env = True。 证明和演绎 在Isabell
7、e/HOL中演绎的形式定义如下： consts pc : exp set exp set -演绎是一个从公式集合到公式集合的函数 syntax pc-derivable : exp set exp bool (infix pc 51) -判断给定公式是否是前提公式集合的演绎结果，符号pc是 为了和通常的数理逻辑教科书中的定义统一 translations pc A A pc() inductive pc() intros ax: A pc A mp: pc A; pc AB pc B 有了上面的形式化定义，不难表示公式A为PC中的定 理，即：axm pc A。若公式A为前提的演绎结果 可表示为
8、：axmpc A。 至此已经建立了命题演算形式系统PC的形式化定义 ，基于该定义作者分析验证与PC有关的性质和定理 。 性质2.1 PC是单调的。即g1 g2 pc g1 pc g2，亦可表达为 g1 g2 pc (axmg1) pc (axmg2)。这由pc的归纳定义不难证得。 定理 2.1（演绎定理）形式化表示为： axmApc B = axmpc AB。 必要性的证明采用了pc上的归纳法；充分性的证明使用分离规则将原 目标分解为两个子目标。两个方向上的证明均使用了pc的定义及前 面已证得的PC的单调性。 性质2.2 A axm trvalue A env = True 即公 理都是永真的
9、。 定理2.2 （PC是合理的）axmpc A env. ( B. B trvalue B env = True) trvalue A env = True 定理2.3 （PC是一致的） (A. axm pc Aaxm pc !A) 定理2.4 （PC 不是完全的）A. A pc axm!A pc axm 主要内容主要内容 定理证明工具Isabelle 命题演算形式系统PC 完备性定理的证明 命题演算形式系统ND 总结 完备性定理的证明完备性定理的证明 关于形式系统完备性的讨论是十分重要的，对命题演 算形式系统PC完备性证明的形式化也是十分必要和 困难的。 采取的技术路线是：先用哥德尔编码完成
10、了用自然数 对PC中的公式编码，同时给出了解码方案并形式验 证了编码的正确性。 将文献5中完备性证明中对=的特殊情况的讨论 扩展到的一般的情形下，定理仍然成立。 完备性定理的证明完备性定理的证明 =的特殊情况： env. trvalue A env = True axm pc A 的一般情况： env. ( B. B trvalue B env = True) trvalue A env = True axmpc A 主要内容主要内容 定理证明工具Isabelle 命题演算形式系统PC 完备性定理的证明 命题演算形式系统ND 总结 命题演算形式系统命题演算形式系统NDND 为叙述方便起见，在I
11、sabelle/HOL中形式化ND系统 时仍采用完备的联结词组和，这并不影响讨论 ND系统的推理和性质，只是在推理规则中略去了与 联结词、和相关的六条推理规则，保留了剩下 的八条。 NDND的形式化定义的形式化定义 consts nd: (exp set) exp) set inductive nd intros nd-axm: B (, B) nd hypI: (, B) nd (A, B) nd hypE: (A, B) nd; (!A, B) nd (, B) nd impI: (A, B) nd (, AB) nd impE: (, A) nd; (, AB) nd (, B) nd
12、negI: (A, B) nd; (A, !B) nd (, B) nd negE: (, A) nd; (, !A) nd; (, B) nd dngI: (, A) nd (, ! !A) nd dngE: (, ! !A) nd (, A) nd 不难证明ND也是合理和完备的，分别形式化表 示为如下两个定理： 定理4.1 nd A env. ( B. B trvalue B env = True) trvalue A env = True 定理4.2 env. ( B. B trvalue B env = True) trvalue A env = True nd A 总结总结 本文针对
13、命题演算形式系统，在机器辅助定理证 明系统Isabelle/HOL中为其建立逻辑模型并对其 正确性进行了形式验证。具体有以下几个方面： 给出了PC的形式化定义，并形式验证了一些重要的性 质和定理及PC的合理性、完备性。 证明了命题演算形式系统ND的正确性。提出了ND的形 式化定义，并形式验证了ND的合理性和完备性。 表表1 1 命题演算形式系统形式化证明的工作量统计命题演算形式系统形式化证明的工作量统计 名称内容代码量（行） 命题演算形式系统PC 包括PC的形式化定义及 重要性质和定理 1741 素数与素数有关的性质和定理2550 歌德尔编码 为PC中公式提供了编、 解码函数并形式化验证了 其正确性 3090 命题演算形式系统ND 包括ND的形式化定义及 重要性质和定理 143 总结总结 通过文中对命题演算两个形式系统PC和ND的分 析和验证，表明采用机器辅助定理证明系统，对 以数理逻辑为平台的各种形式系统进行严格的分 析和证明是可行的。
