命题公式主范式的自动生成与形式输出

在文[1]和文[2]的基础上,给出了命题逻辑中任一命题公式的主析取范式和主合取范式的自动生成算法.并实现了多个命题公式主范式的同时形式化输出.

维普资讯 http://www.77cn.com.cn

第 2第 5期 O卷20 0 6年 9月

甘肃联合大学学报 (自然科学版 )J u n lo n u La h iest ( tr l ce cs o r a fGa s in eUnv ri Nau a in e ) y S

V0 _ O No 5 l2 .Se t 2 06 p. 0

文章编号：1 7—9 X【0 6 0—0 90 6 26 1 20 )504—4

命题公式主范式的自动生成与形式输出张会凌(肃联合大学数学与信息学院，肃兰州 70 0 )甘甘 30 0摘要：文 1 3和文 1 3的基础上，出了命题逻辑中任一命题公式的主析取范式和主合取范式的自动生在 - 1 - 2给

成算法 .实现了多个命题公式主范式的同时形式化输出 .并 关键词：题公式；析取范式；合取范式；命主主自动生成；式输出形中图分类号： 3 1 I TP 0 .文献标识码： A

求一个给定的命题公式的主析取范式 ( S e (p—c 1 i u cieNoma F r简记为 D i )D s n t r l om, a j v NF)与主合取范式 ( S ei1 C nu cie ( p c ) o jn t No ma a v r l

考虑极大项的排列顺序时， F的 C NF是惟一的. 此处为极大项的排列规定一个顺序.于每对

个极大项卢 V卢。。 V… V卢一， 。使其对应一个二进制数 1a…a一，中 2 1 1其 0

F r简记为 C ) om, NF是命题逻辑中一类很重要的工作.因为命题公式的主范式 (主合取与主析取范式的总称) DD是 P分解和进一步进行机器处理的基础.

f,若 P1 P; 0为

【,若卢为一P. 1。 并且规定，应的二进制数小的极大项排在前面 .对

通常求主范式的方法有二.是将已知命题一

二进制数 1a…a一可看成对应极大项的编码 . 2。 0这种规定保证了 C NF表示的惟一性，以及在形式

公式等值变换为所要求的主范式；是列出真值二表后，根据真值表写出相应的极大项和极小项，最后写出主合取范式与主析取范式.给定的命题当公式所含命题变元较多或公式的构成比较复杂时，用这两种方法求其主范式总是有很大的工作量且容易出错 .

上的统一.将 F的真值表“在横排”,左到右后从依次求得极大项后再将其合取，果即与这里的结规定完全一致 .

为了在某种特定的编程语言 ( C语言 )如环

境下形象地输出主范式，约定当两个命题变元或两个子公式之间用逻辑联结符^联结时，“^”可以省去.当它们用逻辑联结符 V联结时，用两而则个半角字符“”/的组合“表示 .辑非的\和“” V”逻

由于我们已经在 E l 2中成功地解决了任 l和E 1一

含 n个变元的命题公式 F的基本真值矩阵 A

和B的生成算法，以及 F的真值表的计算和输出问题，故可在此基础上参考用手工写出主范式的方法，出在计算机上计算和输出主范式的算给

符号“”“”]用！代替 (同)下 .下面给出计算和输出主合取范式的算法模

法.在这里，键是如何根据给定的命题公式按照关要求形式地输出正确的主范式 . 本文仍用 N—S图给出针对所要解决的问题的核心算法，而将源程序略去.

块.假定需要求 N个命题公式 F, l…, 。。 F, F一的主合取范式，基本真值矩阵 B一 (和这 N而 6)个命题公式 F的真值表构成的矩阵 Fv见[] ( 2)已经求出，这里矩阵 F v的第 k行是公式 F的真值.

1主合取范式的自动计算与输出 命题公式 F( 0 P。…,。的主合取范式 P,, P一)C NF是若干关于命题变元 P,,, 。 0 P。… P一的极大项 P。 V… VP一的合取，中 P为 P或 VP。 。其 - 7

为了把永真式 (即重言式 )的主合取范式按 1 输出，把永假式 (即矛盾式 )主析取范式按 0输的出，以流程图 1出一个识别模块 M。先给 . 这样，在这 N个命题公式中，个是永真某

P (一 0 1…,一1, NF必与 F等价. i,, n )C当不收稿日期：0 60—9 2 0—41 .

式当且仅当其对应的 g一1是永假式当且仅当 ,

作者简介：会凌 (9 4)男，肃成县人，肃联合大学数学与信息学院副教授，要从事微分几何与计算机方面张 1 5一，甘甘主的研究.