收稿日期 2006 04 19 作者简介 张会凌 1954 男 甘肃成县人 甘肃联合大学数学与信息学院副教授 主要从事微分几何与计算机方面 的研究 文章编号 1672 691X 2006 05 0049 04 命题公式主范式的自动生成与形式输出 张会凌 甘肃联合大学 数学与信息学院 甘肃 兰州 730000 摘 要 在文 1 和文 2 的基础上 给出了命题逻辑中任一命题公式的主析取范式和主合取范式的自动生 成算法 并实现了多个命题公式主范式的同时形式化输出 关键词 命题公式 主析取范式 主合取范式 自动生成 形式输出 中图分类号 TP301 1 文献标识码 A 求一个给定的命题公式的主析取范式 Spe cial Disjunctive Normal Form 简记为 DNF 与 主合 取 范 式 Special Conjunctive Normal Form 简记为 CNF 是命题逻辑中一类很重要的 工作 因为命题公式的主范式 主合取与主析取范 式的总称 是 DDP 分解和进一步进行机器处理的 基础 通常求主范式的方法有二 一是将已知命题 公式等值变换为所要求的主范式 二是列出真值 表后 根据真值表写出相应的极大项和极小项 最 后写出主合取范式与主析取范式 当给定的命题 公式所含命题变元较多或公式的构成比较复杂 时 用这两种方法求其主范式总是有很大的工作 量且容易出错 由于我们已经在 1 和 2 中成功地解决了任 一含 n 个变元的命题公式F 的基本真值矩阵 An 和Bn的生成算法 以及 F 的真值表的计算和输 出问题 故可在此基础上参考用手工写出主范式 的方法 给出在计算机上计算和输出主范式的算 法 在这里 关键是如何根据给定的命题公式按照 要求形式地输出正确的主范式 本文仍用 N S 图给出针对所要解决的问题 的核心算法 而将源程序略去 1 主合取范式的自动计算与输出 命题公式 F P0 P1 Pn 1 的主合取范式 CNF 是若干关于命题变元 P0 P1 Pn 1的极 大项 P0 P1 Pn 1的合取 其中 Pi为 Pi或 Pi i 0 1 n 1 CNF 必与 F 等价 当不 考虑极大项的排列顺序时 F 的 CNF 是惟一的 此处为极大项的排列规定一个顺序 对于每 个极大项 P0 P1 Pn 1 使其对应一个二进 制数 0 1 n 1 其中 1 0 若 P1为 Pi 1 若 P1为 Pi 并且规定 对应的二进制数小的极大项排在前面 二进制数 0 1 n 1可看成对应极大项的编码 这种规定保证了CNF 表示的惟一性 以及在形式 上的统一 在将 F 的真值表 横排 后 从左到右 依次求得极大项后再将其合取 结果即与这里的 规定完全一致 为了在某种特定的编程语言 如 C 语言 环 境下形象地输出主范式 约定当两个命题变元或 两个子公式之间用逻辑联结符 联结时 可 以省去 而当它们用逻辑联结符 联结时 则用两 个半角字符 和 的组合 表示 逻辑非的 符号 用 代替 下同 下面给出计算和输出主合取范式的算法模 块 假定需要求 N 个命题公式F0 F1 FN 1的 主合取范式 而基本真值矩阵 Bn bij 和这 N 个命题公式F 的真值表构成的矩阵 FV 见 2 已经求出 这里矩阵 FV的第 k 行是公式 Fk的真 值 为了把永真式 即重言式 的主合取范式按 1 输出 把永假式 即矛盾式 的主析取范式按 0 输 出 先以流程图 1 给出一个识别模块 M1 这样 在这 N 个命题公式中 某个 Fk是永真 式当且仅当其对应的 gk 1 是永假式当且仅当 第 20卷第 5期甘肃联合大学学报 自然科学版 Vol 20 No 5 2006年 9 月Journal of Gansu Lianhe University Natural Sciences Sept 2006 图 1 关于永真式和永假式的识别模块 Figure1 An identifying module for tautology and contradiction 其对应的 sk 0 于是在计算出真值表并运行了上面的识别模 块之后 同时计算和输出多个命题公式的主合取 范式的算法模块如图 2所示 图 2 计算和输出多个命题 公式的主合取范式的算法模块 Figure2 Algorithm module calculating and outputting CNF of several propositional formulea 算法中把永真式的主合取范式按 1 输出 必须强调的是 此模块对命题公式的主合取 范式的输出是形式上的 是对手工列真值表 然后 根据真值表写出主合取范式的过程的模拟 主析 取范式 DNF 的输出也是形式上的 2 主析取范式的自动计算和输出 命题公式 F P0 P1 Pn 1 的主析取范式 DNF 是若干关于命题变元 P0 P1 Pn 1的极 小项 P0 P1 Pn 1的析取 其中 Pi为 Pi或 Pi i 0 1 n 1 DNF 必与 F 等价 同 样 当不考虑极小项的排列顺序时 F 的 DNF 是 惟一确定的 为了保证 DNF 在内容和形式上都 惟一 类似地为极小项的排列规定一个顺序 对于每个极小项 P0 P1 Pn 1 使其对 应一个二进制数 0 1 n 1 其中 i 0 若 P1为 Pi 1 若 Pi为Pi 规定对应的二进制数小的极小项排在前面 二进 制数 0 1 n 1可看成对应极小项的编码 假定命题公式的基本真值矩阵 Bn和N 个命 题公式F 的真值表构成的矩阵 FV已经求出 则 计算和输出 N 个命题公式的主析取范式的算法 如图 3 所示 算法中把永假式的主析取范式按 0 输出 在主析取范式中 极小项用圆括号括起来 各 个极小项之间是用析取符号 联结的 标志变 量 r 的作用是为了避免在最后一个极小项的右括 号 之后再打印一个多余的 例 给出两个命题公式 F0 P0 P1 P2 P3 和 F1 P0 P1 P2 P3 求它们的主合取范式与主析取范式 将所给的两个命题公式输入 依据上面的算 法编程运行 则系统有如下的输出结果 公式 F0和 F1的真值表是 如 2 所示 输 出的真值表是一般的教科书上的真值表的 转 置 P 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 P 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1 P 2 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 P 3 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 F00 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 50 甘肃联合大学学报 自然科学版 第 20卷 F10 1 1 0 0 1 1 0 0 1 1 0 1 1 1 1 图 3 计算和输出多个命题公式的主析取落式的算法模块 Figure3 Algorithm module calculating and outputting DNF of several propositional formulae 公式 F0的主合取范式是 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 公式 F1的主合取范式是 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 公式 F0的主析取范式是 P0 P1 P2 P3 公式 F1的主析取范式是 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 P0 P1 P2 P3 尽管所给的例子中只有 4 个命题变元 用手 工计算列出的真值表也有 16 行 直接计算主合取 范式和主析取范式进行核对 可知程序输出的结 51 第 5 期 张会凌 命题公式主范式的自动生成与形式输出 果是完全正确的 当命题变元数 n 5 时 自动计算和输出主范 式的优点显得尤为突出 本文所给的算法已在 C 语言和VC 环境下完 全实现 参考文献 1 张会凌 命题逻辑判定系统中基本真值矩阵的生成算 法 J 甘肃联合大学学报 自然科学版 2005 19 1 16 19 2 张会凌 命题公式真值表的生成与公式类型的机械判 定 J 甘肃联合大学学报 自然科学版 2006 20 1 25 34 Automatic Generation and Formal Output of Special Normal Forms of Propositional Formulae ZH A NG H ui ling School of Mathematics and Information Gansu Lianhe University Lanzhou 730000 China Abstract Based on paper 1 and 2 this paper gives two generating algorithms to calculate and out put the special conjunctive normal forms and special disjunctive forms of given propositional formulas automatically and formally Key words propositional formula special conjunctive normal form special disjunctive normal form au tomatic generation formal output 上接第 3 页 6 教育部办公厅 高等学校学报管理办法 S 中国高等学报自然科学学报研究会 会讯 1998 总 30 封二 7 孙德存 地方高校的本地化定位 J 吉昌学院学报 2004 4 72 74 8 窦炎国 周继红 努力为地方经济 社会服务 J 苏州科技学院学报 社科版 2004 21 3 135 138 Exploratory Advancing and Pioneering Innovating teaching scientific research training of talent explora tion review 52 甘肃联合大学学报 自然科学版 第 20卷

展开阅读全文