數(shù)理邏輯中命題公式等價證明的程序化研究與實現(xiàn)

楊劍蘭 周青

（昆明醫(yī)科大學(xué)海源學(xué)院 云南省昆明市 650106）

邏輯學(xué)是研究思維形式、思維規(guī)律的科學(xué)，其中思維形式結(jié)構(gòu)包括對事物的概念單位呈現(xiàn)、屬性肯定或否定的判斷和由此產(chǎn)生的關(guān)聯(lián)推理；思維規(guī)律是指在思維過程中必須遵守的法則，這些法則是保證思維符合正確發(fā)展的必要條件，對思維的無限延伸和發(fā)散具有科學(xué)地制約作用。以數(shù)學(xué)方法、建立符號和運(yùn)算式來研究推理規(guī)律、展現(xiàn)推理過程，則為數(shù)理邏輯。數(shù)理邏輯的奠基人萊布尼茨提出：

（1）建立如同“數(shù)學(xué)的符號”的一種通用語言，這種語言中每一符號表示一個概念；

（2）并確立一個完善的邏輯演算體系，演算是根據(jù)確立的邏輯規(guī)則進(jìn)行符號運(yùn)算。

以上兩點正是數(shù)理邏輯的基本特征[1]，而以符號依據(jù)相應(yīng)標(biāo)準(zhǔn)來表示自然事物的結(jié)構(gòu)則為命題公式。萊布尼茲還提出了“不可分辨同一性”原理，即一個元素能被另一元素所替換而保持原命題的真值，那么它們就是同一的[2]，可理解為用于表示一件事物的符號與連結(jié)詞不止一種，即命題公式是存在相互等價的。本文以真值表法判斷兩個命題公式等價與否，并結(jié)合計算機(jī)語言程序設(shè)計將求解過程以計算機(jī)工具實現(xiàn)對兩組包含兩個及以上命題變項的任意命題公式的等價判斷，從而體現(xiàn)現(xiàn)代計算機(jī)科學(xué)技術(shù)處理數(shù)理邏輯問題的能力，啟迪更多的學(xué)習(xí)者深刻理解理論發(fā)展與應(yīng)用之間的關(guān)聯(lián)。

1 命題公式

1.1 命題

屬性可在真假之一判定的陳述句被稱為命題，用自然語言表示的命題在數(shù)理邏輯中可用符號進(jìn)行表示，并且每條命題對應(yīng)可判斷的真值，成立為真（T，1），不成立為假（F，0）。不可再進(jìn)行邏輯結(jié)構(gòu)分割的命題為原子命題，由原子命題組成的命題為復(fù)合命題。如表1。

表1：判斷語句是否是命題的例題

數(shù)理邏輯的主要使命是消除自然語言的局限性和不規(guī)則性，創(chuàng)建具有簡明符號、合理規(guī)則的“通用語言”，為此，萊布尼茨做了兩方面的努力：一是尋找能夠代表所有概念并可認(rèn)作最根本的不可分析的符號，對應(yīng)原子命題；二是給出表述諸如斷定、合取、析取、否定、全稱、特殊、條件聯(lián)結(jié)等形式概念的設(shè)計，對應(yīng)連結(jié)詞[2]，由連結(jié)詞和原子命題構(gòu)成復(fù)合命題。如表2。

表2：命題的符號化

表2 中三道命題均因明確對應(yīng)的語句而具備確定真值，則為命題常項。而基于符號層面剝離自然語境是進(jìn)行數(shù)理推演是數(shù)理邏輯的使命和目的，因此在對一串符號進(jìn)行推導(dǎo)和演算具體真值結(jié)果時，往往是對組合成該命題的各個元素做不同情況的真值指派，再結(jié)合出現(xiàn)的連結(jié)詞和法則推算，如表3。

表3：復(fù)合命題p →q 真值與組成符號真值的關(guān)系

由表3 可見，復(fù)合命題p →q 真值由其所包含的原子命題以及連結(jié)詞的具體真值指派決定，某些情況下使其為T，某些情況下為F。即p 與q 的真值可以代入不同的原子命題及相應(yīng)的T/F 值，則p、q 為命題變項。

1.2 命題公式及其等價判斷

命題公式是對由命題常項，命題變項、聯(lián)結(jié)間和括號按照一定邏輯關(guān)系構(gòu)成的復(fù)合命題的形式化描述。命題公式本身不是命題，沒有真值，只有對其命題變項進(jìn)行賦值后，它才有真值。兩組命題公式A 與B 即使構(gòu)成形式上不一致，但只要對包含的全部n 個命題變項作2n組真值指派后，所有同一組真值指派后得到的命題公式A 與B 真值完全相同，則A 與B 等價。例如表4。

表4：命題公式q →(p∨(p∧q))與q →p 真值表

從表4 可見，命題公式q →(p∨(p∧q))與q →p 形式雖不相同，但在四組對p，q 的不同真值指派組合下得到的真值完全一致，則命題公式q →(p∨(p∧q))與q →p 等價。

2 計算機(jī)程序化

2.1 計算機(jī)程序與離散數(shù)學(xué)關(guān)系簡述

計算機(jī)程序是一組有序指令的集合，是用來定義計算機(jī)指令執(zhí)行流程的形式化語言。每種程序語言都包含一整套詞匯和語法規(guī)范，這些規(guī)范通常包括數(shù)據(jù)類型和數(shù)據(jù)結(jié)構(gòu)、指令類型和指令控制、調(diào)用機(jī)制和庫函數(shù)以及不成文的規(guī)定（如遞進(jìn)書寫、變量命名等）[3]。離散數(shù)學(xué)思想與計算機(jī)程序?qū)壿媶栴}的處理密切關(guān)聯(lián)，并且能反映事物本身在微觀視角的離散特性下存在與運(yùn)行的機(jī)制。Curry-Howard 同構(gòu)顯示了推理系統(tǒng)和程序語言之間的相似性[4]，命題即類型，證明即程序，在直覺主義邏輯中，所有基于形式化方法構(gòu)造的證據(jù)寫成的命題證明，都可以解釋為一個具有類型的程序交由計算機(jī)進(jìn)行驗證。

2.2 連結(jié)詞與程序邏輯運(yùn)算符

（1）﹁（取反），∧（合?。?，∨（析取）三種最為基本和簡單的邏輯連結(jié)詞與對應(yīng)的程序語言邏輯運(yùn)算符如表5。

表5：命題連結(jié)詞與對應(yīng)的Java 語言邏輯運(yùn)算符

（2）→（蘊(yùn)含），?（當(dāng)且僅當(dāng)）連結(jié)詞的邏輯性質(zhì)符合以下程序分支結(jié)構(gòu)，如表6。

表6：命題連結(jié)詞與對應(yīng)的Java 程序分支結(jié)構(gòu)示例

（3）也可根據(jù)等價關(guān)系，將p →q 轉(zhuǎn)化為﹁p∨q，將p?q 轉(zhuǎn)化為(﹁p∨q)∧(p∨﹁q)再進(jìn)行后續(xù)運(yùn)行。

2.3 對應(yīng)計算機(jī)程序思路

（1）面向?qū)ο蟪绦蛟O(shè)計構(gòu)成模塊的基本單元是類，可基于一個類的屬性創(chuàng)建不同的具體對象，并且在類中創(chuàng)建不同的運(yùn)行機(jī)制（方法）供不同對象反復(fù)調(diào)用。為能夠?qū)崿F(xiàn)兩組及以上命題公式的等價判斷，可使用面向?qū)ο蟪绦蛟O(shè)計功能，基于命題公式類創(chuàng)建兩個命題公式對象A 與B；

（2）建立for 循環(huán)遍歷用戶輸入的公式對象中各個元素，并利用棧結(jié)構(gòu)來實現(xiàn)把公式從中綴表達(dá)式轉(zhuǎn)換為后綴表達(dá)式便于運(yùn)算，如a+b*(c+d*e)-f 轉(zhuǎn)換為abcde*+*+f-；

（3）在后綴表達(dá)式中判斷命題變元的數(shù)量n；

（4）將n 個命題變元共2n真值存儲在數(shù)組中，循環(huán)遍歷輸出真值表；

（5）讓A 與B 分別調(diào)用上述已構(gòu)造好的方法；

（6）對得到的兩組命題公式真值做遍歷匹配，若完全一致則兩組公式等價。

程序核心代碼如下：

2.4 上機(jī)驗證

例題：求解命題公式q →(p∨(p∧q))與q →p 是否等價，在IDEA 下運(yùn)行結(jié)果正確，如圖1。

圖1：Java 程序運(yùn)行結(jié)果

3 結(jié)語

萊布尼茨對邏輯問題的最早探索和最初貢獻(xiàn)是試圖沿著笛卡爾和霍布斯的思路建構(gòu)所謂的“通用語言”，這是一套表達(dá)思想和事物的符號系統(tǒng)[2]，正因如此，也為計算機(jī)工具自動化實現(xiàn)邏輯問題的求解奠定了數(shù)學(xué)基礎(chǔ)；而計算機(jī)科學(xué)家如阿倫?凱所發(fā)明的面向?qū)ο蟪绦?，為計算機(jī)程序求解基于同類創(chuàng)建的不同個體實例提供了便利，才使計算機(jī)程序證明兩套命題公式是否等價得以高效地實現(xiàn)。阿爾伯特?愛因斯坦說過：“所有科學(xué)的宏大目標(biāo)都是：從最小數(shù)量的假說或公理出發(fā)通過邏輯演繹推理說明最大數(shù)量的實驗事實”，學(xué)習(xí)和認(rèn)識邏輯演繹推理并能夠擅長使用現(xiàn)代計算機(jī)手段進(jìn)行相關(guān)問題的處理可以在很大程度上幫助學(xué)習(xí)者以工學(xué)應(yīng)用為導(dǎo)向地進(jìn)入科學(xué)世界。