维普资讯 http://www.cqvip.com ２００８年第３期 福建 电脑 命题公式类型的判定 林运国 ．徐荣聪’ ｆ１．福州大学数学与计算机科学学院福建福州３５０００２ ２．福建农林大学计算机与信息学院福建福州３５０００２） 【摘要】：本文提出如何判断一个公式为重言式、矛盾式、可满足式的方法。基于遗忘理论提出遗忘合式公式方法，在 保持逻辑等值的条件下。遗忘掉公式的冗余命题变元，使得公式包含更少的命题变元，为判定命题公式类型提供一种能行的 方法。 【关键词】：重言式；矛盾式；可满足式；遗忘理论 １、前言 满足ｔ，， ， 。它体现在Ｐ 指派为１任何指派必然可以找 要判定一个合式公式是否为重言式：矛盾式或可满足式，常 到一个指派，该指派除了ｌＯ，指派为０外其余命题变元指派都相 用的方法有真值表法、垂直路径法或主范式ｌＩ１，但是公式所含命 同，且公式Ａ能够取到相同的真值。并且可以看出Ａ（ｐ ，１ ）可 题变元较多时．这些方法实际操作起来都是相当得麻烦。文献日 以用来表示ｆｏｒｇｅｔ（Ａ，ｐ￣）。当然Ａ（Ｐ／ｆａｌｓｅ）也是可以用来表示 则提供了利用计算机对有限多个命题公式的真值表的直接计算 ｆｏｒｇｅｉ（Ａ，ｐ￣）。故不妨取Ａ（ｐ／ｔｒｕｅ）ＶＡ（ｐ／ｆａｌｓｅ）来表示ｆｏｒｇｅｔ（Ａ， 和输出．并对一个命题公式是否为重言式、矛盾式或可满足式给 ｐｉ）ｏ 出判定．但较为复杂。Ｌｉｎ Ｆａｎｇｚｈｅｎ和Ｒａｙ Ｒｅｉｔｅｒ提出的遗忘理 上述定理提供了计算ｆｏｒｇｅｔ ，ｐ）的方法。下面结合定理２ 论『３１详细描述了当一个事实不再正确以及对未来不再产生影响 给出判定一个命题变元是否为冗余变元的简便方法。 时．需要把这个事实和它所存在关系进行遗忘。本文基于这个理 定理３：公式Ａｌｐ ·ｐ＾『是可以遗忘掉命题变元Ｐ ，当且仅 论提出了判定合式公式为重育式、矛盾式或可满足式的一种能 当公式 行办法。 Ａ（ｐ／ｔ￣） （ｐｆｆａ／ｓｅ）为重言式。 ２、合式公式的遗忘理论 证明：对ｐ ·ｐ 任取一组值，Ｐ－不论取ｔｒｕｅ或 ｅ，Ａ ／ 定义１：设５＝ ＾Ｐ ·ｐ＾『，作ｒ（ｓ）￣ｎＹ： ｔｒｕｅ）与Ａ（ｐｆｆａｌｓｅ）保持相同的真值，所以Ａ（ｐ／ｔｒ￣） （Ｐ／ （ｉ 』 … Ｅ厂ｆｓＪ； ｆａｌｓｅ）为重言式。 （ｉｉ）若Ａ，Ｂ Ｅ， Ｓ ，贝Ｕ ，ＡＶＢ，Ａ人Ｂ，Ａ—Ｂ，ＡｓＢ Ｅ， ； 性质１：重言式或矛盾式的任何一个命题变元都是冗余变 （ｉｉｉ）凡属于厂ｒｓＪ的元都可通过（ｉ）和（ｊｉ）得到，则称厂 元。 为．ｓ生成的（Ｖ，Ａ，一， 型公式集，ｓ中的元Ｐ称为命题变元或 该性质结合定理３提供了判定一个公式是否为重言式、矛 原子公式。ｒ（ｓ）Ｏ的元Ａ ．ｐ 称为合式公式，简称公式 。 盾式、可满足式的方法。具体表述如下：要判定一个命题公式的 定义２：设，若ｖ：ｒｒｓ ｛Ｏ，１ｌ是同态的，则称ｖ为厂 的赋 类型。首先假定它为重言式。这样每个命题变元都可以看作是冗 值。ｔ，。 ）为公式Ａ在．ｓ上赋值，全体赋值之集记为Ｑ『 。 余变元。接下来逐个遗忘掉每个命题变元，直到遗忘掉最后一个 定义３：设厂ｆ 为公式集，Ｐ Ｅ ｓ，Ａ Ｅ厂ｆｓＪ，若ｔ，， 砷 ，则 命题变元。如果得到的是ｔｒｕｅ。则说明该合式公式为重言式；如 称公式Ａ可遗忘掉命题变元Ｐ．同时称Ｐ为公式Ａ的冗余命题 果得到的是 ｓｅ，则合式公式有可能是矛盾式或可满足式。对于 变元（简称冗余变元）；记Ａ￣－ｆｏｒｇｅｔ（Ａ，ｐ），Ａ 为公式Ａ可遗忘命 后一种情况还可以进一步判定。因为矛盾式的否定是重言式。所 题变元ｌ的结果。 以可在原合式公式前加个否定词．按照上面方法继续判定变形 例１：公式Ａｒｐ ＡｇＪＶ Ａｑ）－－＊ｒ 后的合式公式是否为重言式．如果是则说明原合式公式为矛盾 不难看出公式Ａ与口一ｒ是逻辑等值的，公式Ａ可遗忘掉 式．否则就是可满足式。 命题变元ｐ ｒｇｅｔ（Ａ ：ｇ—ｒ。 例２：判定Ａ 一 人ｒ广 人 Ｖ ｒｑＶ５Ｊ为重言式。 定理１：若Ａ ￡ ，ｐＪ当且仪当可以化为合（析）取范式， 第一步遗忘得：ｑＶ 卜 卜 Ｖｓ）Ｖ 卜 人广＋ｑＶ５ ； 且每一项要么含有Ｐ人 （Ｐ人］Ｐ）要么不含Ｐ或 ，删掉虚式， 第二步遗忘口得： ｓ）人广 ； 则合（析）取范式不再含有命题变元 第三步遗忘ｒ得：５ ： 通过这个定理可以用来判定在一个合式公式中命题变元是 第四步遗忘５得：ｔｒｕｅ。 否为冗余变元，并且可计算出ｆｏｒｇｅｔ（Ａ，ｐＪ。但一个包含多个命题 变元的公式要化为合（析）取范式，不是一件容易的事。那么如何 参考文献： 比较方便地计算出ｆｏｒｇｅｔ ，ｐ），下面给出一个定义和一个定理可 １．王兵山张强李舟军．数理逻辑ｆＭ１．长沙：国防科技大学出版社．１９９３． 以方便得计算出ｆｏｒｇｅｔ（Ａ，ｐ）。 ４６－５６． 定义４：设公式Ａ Ｅ ｒ（ｓ￣ｐ Ｅ５，记Ａ（ ，ｔ ） （ｐ／ｆａｌｓｅ））分别 ２．张会凌．命题公式真值表的生成与公式类型的机械判定珊．甘肃联合 表示公式Ａ中凡出现Ｐ均代换为ｔｒｔｔｅ（ｆａｌｓｅ）。进一步，若ＴＣＦ 大学学报（自然科学版） ２００６，２０（１）：２５－２７． ３．ＦａｎｇｚｈｅｎＬｉｎ ａｎｄＲ．Ｒ．ｅｉｔｅｒ．Ｆｏｒｇｅｔｉｄ ｏ１ ，记Ｔ（ｐ／ｔｎａｅ）（Ｔ（ｐ／ｆａｌｓｅ） 表示在公式集 的每个公式凡有出 现Ｐ均代换为ｔｒｕｅ（ｆａｌｓｅ）。 Ｗｏｒｋｉｎｇ Ｎｏｔｅｓ ｏｆ Ａ从Ｉ Ｆａｌｌ ｓｙｍｐｏｓｉｕｍ ｏｎ Ｒ．ｅｌｅｖａｎｃｅ．１９９４：１５４－１５９． 定理２：设公式Ａｌｐ ·ｐ＾『是可遗忘掉命题变元Ｐ ，则 ４．孙明汀．数学逻辑【Ｍ１．长沙：中南大学出版社，２００４．３２－３６． ５．王国俊．数理逻辑引论与归结原理ｉＭ１．北京：科学出版社．２００６．１８－２０． ｙｏ，ｇ￣（Ａ， ）＝ Ａ／ｔｒｕｅ）ｖ Ａ／ ６．Ｆａｎｇ＇ｚｈｅｎ Ｌｉｎ．Ｏｎ Ｓｔｒｏｎｇｅｓｔ Ｎｅｃｅｓｓａｒｙ ａｎｄ Ｗｅａｋｅｓｔ Ｓｕ ｃｉｅｎｔ Ｃｏｎｄｉｔｉｏｎｓ 证明：设ｐ ·ｐ 是Ｉ１，个不同的命题变元，Ａｌｐ￣，ｐ ·ｐ＾『为ｎ Ⅱ１．Ａｒｔｉｉｆｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ，２００１。１２８：１４３—１５９． 元合式公式。因为公式Ａ是可以遗忘掉．命题变元Ｐ ，所以必须 基金项目：福州大学较人才基金（ＸＲＣ一－０６１８）
