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

楊劍蘭 周青

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

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

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

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

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

1 命題公式

1.1 命題

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

表1：判斷語(yǔ)句是否是命題的例題

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

表2：命題的符號(hào)化

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

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

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

1.2 命題公式及其等價(jià)判斷

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

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

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

2 計(jì)算機(jī)程序化

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

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

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

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

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

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

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

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

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

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

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

（3）在后綴表達(dá)式中判斷命題變?cè)臄?shù)量n；

（4）將n 個(gè)命題變?cè)?n真值存儲(chǔ)在數(shù)組中，循環(huán)遍歷輸出真值表；

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

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

程序核心代碼如下：

2.4 上機(jī)驗(yàn)證

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

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

3 結(jié)語(yǔ)

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