收稿日期 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卷

展開閱讀全文

總結

以上是生活随笔為你收集整理的命题公式的主合取范式C语言,命题公式主范式的自动生成与形式输出.pdf的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。