數理邏輯中范式推算的程序化研究與實現

楊劍蘭，周青

（昆明醫科大學海源學院，云南 昆明650106)

0 引言

離散數學是研究有離散結構的系統的學科，譬如，繪制一條直線段的墨水痕跡并非連續，而是由有限多個離散的點組成，這與人類一貫的認知不同。而當計算機打印這條線段時就是以打點的方式打印出來的[1]，因此離散數學思想與計算機工作原理密切關聯，并且更加符合萬事萬物本身的底層特性。其中數理邏輯部分是用符號的方法研究關于命題推理、證明等的問題。丘成桐曾說：“大道至簡，是對數學之美的歸納，最簡單的數學，從1=1開始，到1+1=2，1+2=3，不停推導下去。人類通過這種方式，認識到自然數，從而有了數學”[2]。因此，在數理邏輯中“邏輯”是一種形式語言，用于表示能得出結論的信息，邏輯問題可轉變為由符號與連接詞構成的命題公式，并且進一步轉換為等價的標準范式，通過標準范式可輕易實現排除錯誤的邏輯關系、找到符合問題本身邏輯的命題狀態，快速達到實現推理和證明出準確結論。

本文針對求解命題公式的主析取范式與主合取范式，在真值表法基礎上，分析解釋了構造析?。ê先。┓妒綍r以成真（假）指派反推對應?。ù螅╉椀脑?，并結合計算機語言程序設計將該解法從理論求解遷移至計算機工具求解，給出了程序設計的具體流程和代碼，從而更好地實踐“以解決問題為導向掌握和運用工具”學習模式以及幫助學習者建立定理自動化證明的認知，進一步理解人工智能基礎。

1 范式

在布爾邏輯中，主析取范式與主合取范式是邏輯公式的標準規范化，其中主析取范式是由各個所涉及命題變元的合取子句即最小項的析??；主合取范式是由各個所涉及命題變元的析取子句即最大項的合取。作為規范形式，它們在自動定理證明中發揮作用，在邏輯問題中將局面直觀展現以更清晰地推出結論。比如，以下邏輯謎題：A，B，C，D 四人中要派兩人去參加教學比賽，按下述三個條件有幾種派法？如何派？

1) 若A去，則C和D中要去一人；

2) B和C不能都去；

3) C去則D留下。

將命題A，B，C，D 分別表示A 參加、B 參加、C 參加、D參加，則該邏輯謎題轉換為命題公式：

(A→((C∧?D)∨(?C∧D)))∧?(B∧C)∧(C→?D)，進一步轉化為等價主析取范式并刪去與題意矛盾的項目后得到：(?A∧B∧?C∧D)∨(A∧?B∧?C∧D)∨(A∧?B∧C∧?D)，故派法為：B∧D，或A∧D，或A∧C。共三種派法。

2 計算機程序化

2.1 范式連結詞與程序邏輯運算符

通過命題公式的等價轉換，任何連結詞都可轉換為：?（取反），∧（合?。?，∨（析?。┤N最為基本和簡單的連結關系，在主析取范式和主合取范式中，規定只能含有以上三種連結詞，并且每個符號右邊須緊跟單個命題變元。在計算機Java 程序中有三個基本的邏輯運算符與該三個連結詞對應，如表1。

表1 命題連結詞與對應的Java語言邏輯運算符

當命題公式中含有→（蘊含），?（當且僅當）連結詞時，根據連結詞邏輯性質特征，可得出對應的程序語句，如設置前提為P，后件為Q，則P→Q真值符合以下規律：if(!P){(P→Q)=true;}；if(Q){(P→Q)=true;}。P?Q真值符合以下規律：if(P){if(Q){(P?Q)=true;}}else{ if(!Q){(P?Q)=true;} }。

2.2 真值表法求主析?。ê先。┓妒?/h3>

n 表示命題變元數量，求解主析取范式與主合取范式，利用真值表法可歸為以公式成真或成假賦值反推所對應的包含n 個命題變元的各個小項組mi的真值指派問題，為方便觀察公式成真和成假時各命題變元的真假狀態，范式需包含對所有命題變元的規范整理，在構造主析取范式時：結合析取式的特征，能夠使析取式成假的真值指派條件較為苛刻，只有一組m0∨m1∨...mi在等價于F 時可使所有構成析取范式的小項為假，但此時對應的滿足為假的小項組太多，為2n-1組，過于煩瑣。如命題公式(?P∧Q)∨?R，其真值表如表2。

表2 命題公式(?P∧Q)∨?R真值表

當(?P∧Q)∨?R 為0，對應的P，Q，R 真值指派有3組，為序號②，⑥, ⑧，如：此時序號②對應表3。

表3 (?P∧Q)∨?R為0時對應的P，Q，R真值指派組②

此時為1的小項唯有?P∧?Q∧R，其余可構造出真值為0的小項23-1=7項，運算量大效率低下；

而當(?P∧Q)∨?R 為1，對應的P，Q，R 真值指派有5 組，為序號①，③, ④，⑤，⑦，如：此時序號①對應表4。

表4 (?P∧Q)∨?R為1時對應的P，Q，R真值指派組①

根據P、Q、R 三個命題變元的真值指派0、0、0，只可構造出真值為1的小項1項，即?P∧?Q∧?R，除此之外剩余小項23-1=7項為0，運算量小效率高。

因此在構造主析取范式時，采取其真值表中公式成真指派時所對應的最小項的析取式，可反推此時至少有一組所包含的小項值為真，由此精準構造唯一一組對應的小項，將公式所有成真指派時對應的各個唯一小項析取，就能更高效地得到值為真的主析取范式。在構造主合取范式時：結合合取式的特征：能夠使合取式成真的真值指派條件較為苛刻，只有一組，在該組真值賦值下，可使所有構成合取范式的大項為真，才能滿足使合取范式為真，但大項為真對應的大項組太多，為2n-1組，過于煩瑣，因此在構造主析取范式時，采取其真值表中成假指派所對應的最大項的合取式?？煞赐拼藭r至少有一組所包含的大項值為假，由此精準構造唯一一組對應的大項，將公式所有成假指派時對應的各個唯一大項合取，就能更高效地得到值為假的主合取范式。

基于上述原因，得出定理：

1) 一個公式的真值為T(1) 的指派所對應的小項的析取即為此公式的主析取范式[3]；

2) 一個公式的真值為F(0) 的指派所對應的大項的合取即為此公式的主合取范式[3]。

3 用計算機程序求解命題公式的主析?。ê先。┓妒?/h2>

3.1 算法思想

1) 統計命題公式的變元數量n，利用多重for循環給出所有n個變元所有真值指派2n個組合；

2) 使用數組保存所有命題變元真值指派下公式的真值；

3) 根據定理，構造主析?。ê先。┓妒?。

3.2 對應程序思路

1) 將用戶輸入的中綴表達式進行for 循環將公式中的字符遍歷，并轉換為逆波蘭表達式用棧來存儲；

2) 在逆波蘭表達式中判斷命題變元的數量；

3) 將n 個命題變元共2n個真值組存儲在數組中，循環遍歷輸出真值表；

4) 求主析?。ê先。┓妒綍r：當命題公式真值為1(0) 時對應的變元的合?。ㄎ鋈。┙Y果即?。ù螅╉棏獮槌烧妫伲?，根據?。ù螅╉椥再|，應讓每一個對應的變元當前值改造為真（假），則若對應變元值為0(1) 輸出此變元的非（變元），否則直接輸出變元（變元的非），變元與變元之間用合?。ㄎ鋈。┻B結詞連結，項與項之間用析?。ê先。┞摻Y詞連接。

程序核心代碼如下：

3.3 上機驗證

求解命題公式(?P∧Q)∨?R的主析?。ê先。┓妒?/p>

在IDEA下運行結果正確，如圖1：

圖1 Java程序運行結果

4 結束語

符號主義人工智能的思維對應于人類的演繹式思維[4]，而邏輯演繹的符號形式化即數理邏輯，主析?。ê先。┓妒阶鳛閿道磉壿嬛袠O為有價值的命題公式呈現方式，將包含多個命題變元的公式以滿足解讀規范的標準連結了各個命題變元與連結詞。求解主析?。ê先。┓妒降姆椒ㄓ姓嬷当矸ㄒ约暗戎笛菟惴?，其中真值表法對應的求解過程更貼合計算機對離散量處理的方式，同時，人類智能本身就是在各個層次上使用符號，如抽象思維、邏輯、語言，因此符號人工智能研究在某種意義上就是對人類理性思維的研究[5]，理解真值表法的求解思路并轉換為對應的程序語言對培養人類自身計算思維與認識人工智能都有很大的幫助。