命題公式主析范式的自動生成系統(tǒng)

 1 選題背景
邏輯學(xué)是研究思維和論證的科學(xué)，也就是研究關(guān)于人類推理的學(xué)問。在20世紀(jì)的下半個世紀(jì)，伴隨著計算機(jī)科學(xué)技術(shù)的迅猛發(fā)展，新的邏輯學(xué)分支——數(shù)理邏輯也發(fā)展起來。數(shù)理邏輯也稱為符號邏輯，是一門運(yùn)用數(shù)學(xué)的方法來研究推理的形式結(jié)構(gòu)和推理規(guī)律的邊緣性學(xué)科。其內(nèi)容相當(dāng)廣泛，包括邏輯演算（命題演算與謂詞演算）、公理集合論、證明論、遞歸函數(shù)論等，其中邏輯演算是其它各部分的基礎(chǔ)。它在邏輯電路、自動控制、人工智能、程序設(shè)計、數(shù)據(jù)庫理論以及計算機(jī)科學(xué)的其它領(lǐng)域有著廣泛的應(yīng)用。人工智能是研究使計算機(jī)來模擬人的某些思維過程和智能行為，主要包括計算機(jī)實(shí)現(xiàn)智能的原理、制造類似于人腦智能的計算機(jī)，使計算機(jī)能實(shí)現(xiàn)更高層次的應(yīng)用。人工智能涉及的計算機(jī)科學(xué)、心理學(xué)、哲學(xué)和語言學(xué)等學(xué)科。但最主要的依然是計算機(jī)科學(xué)的范疇，人工智能對于邏輯的計算十分依賴，尤其是進(jìn)行推理的時候，在這方面對命題邏輯的研究就有著十分重要的貢獻(xiàn)，它是人工智能所能發(fā)揮的作用有多大，所能覆蓋的范疇有多廣的決定性因素之一，所以求一個給定的命題公式的主析取范式或主合取范式是命題邏輯中一類很重要的工作，它是命題分解和進(jìn)一步進(jìn)行機(jī)器處理的基礎(chǔ)。通過這個系統(tǒng)，用戶可以更加方便的得出命題公式主范式，有助于對命題邏輯的學(xué)習(xí)和研究。
2 研究內(nèi)容
本文主要介紹了命題公式主范式的自動生成方法。首先，給出了主范式的基礎(chǔ)定義及相關(guān)定理，并對其中定義給出解釋，定理做出解釋；探討出主范式的求法——真值表求法，并對設(shè)計過程加以描述，包括了命題公式識別，命題公式轉(zhuǎn)譯以及命題公式真值表生成三個部分，可以實(shí)現(xiàn)命題公式的合法性判斷，大小項的生成，命題公式的真值以及命題公式主范式的生成。
3 概念描述
3.1 大項與小項 小項：n個命題變元的合取式，稱作布爾合取或小項，其中每個變元與它的否定不能同時存在，但兩者必須出現(xiàn)且僅出現(xiàn)一次。
大項：n個命題變元的析取式，稱作布爾析取或小項，其中每個變元與它的否定不能同時存在，但兩者必須出現(xiàn)且僅出現(xiàn)一次。
3.2 主析取范式及主合取范式 主析取范式：對于給定的命題公式，如果有一個等價公式僅由小項的析取所組成，則該等價式稱作原式的主析取范式。
主合取范式：對于給定的命題公式，如果有一個等價公式僅由大項的合取所組成，則該等價式稱作原式的主合取范式。
3.3 主析取范式及主合取范式的求取方法 主析取范式及主合取范式的求取方法有真值表法、等價變換法等，本系統(tǒng)采用真值表法求取主析取范式及主合取范式，故只對這種方法加以描述，其他方法在這里概不描述。
在真值表中，一個公式的真值為T的指派所對應(yīng)的小項的析取，即為此公式的主析取范式。
在真值表中，一個公式的真值為F的指派所對應(yīng)的大項的合取，即為此公式的主合取范式。
4 模塊設(shè)計
由于無法保證用戶輸入一定準(zhǔn)確無誤，而主范式求取的算法默認(rèn)所得到的命題公式是正確的，所以一旦命題公式輸入出錯，則有可能輸出錯誤的結(jié)果，甚至引起本系統(tǒng)的崩潰，所以為了確保程序能正常進(jìn)行，在進(jìn)行主范式生成運(yùn)算前必須驗(yàn)證命題公式是否正確。
由于計算機(jī)的計算速度和存取速度十分快速，而真值表法求取主析取范式及主合取范式實(shí)現(xiàn)起來比較簡單，所以選用了真值表法。這就需要模擬出一個可以填入和修改真值的真值表，最終利用真值表得出命題公式大小項進(jìn)而得出主范式。
因此主范式生成包括公式識別、真值表生成以及主范式生成三大模塊。其中公式識別分為公式格式化、公式轉(zhuǎn)譯、公式化簡并判斷。真值表生成分為真值表初始化，真值表填入。模塊圖如圖1所示。
5 系統(tǒng)實(shí)現(xiàn)
首先給出主范式生成的流程圖。如圖2所示。
5.1 命題公式的識別 命題公式識別算法采用遞歸思想對字符串進(jìn)行重復(fù)簡化直到變成一個命題變元，如果不能則判斷該字符串不是命題公式。
我們知道，命題公式需要遵循四個規(guī)定：
（1）單個命題變元是一個合式公式；
（2）如果A是合式公式，則□A是合式公式；
（3）如果A和B是合式公式，那么（A∧B），（A∨B），（A→B）和（A□B）都是合式公式；
（4）當(dāng)且僅當(dāng)能夠有限次地應(yīng)用（1），（2），（3）所得到的包含命題變元，連接詞和括號的符號串是合式公式。
由于該公式的定義是由遞歸的形式給出的，那么我們依然可以應(yīng)用遞歸思想去對公式進(jìn)行判斷。
為方便系統(tǒng)識別，我們首先定義以下標(biāo)準(zhǔn)：
1）所有的字母使用字符“*”代替；
2）除 “□”符與括號之外的所有符號均使用“@”代替。
當(dāng)傳入字符串之后，首先去掉空括號與連續(xù)的兩個“□”符，之后運(yùn)用上述標(biāo)準(zhǔn)做字符替換。由于我們的工作是判斷該字符串是否是一個合法的命題公式，在判斷的最后只需要返回一個true值或者false值。也就是說A與（A∧B）的返回值是一樣的。
在這里我們編寫了一個剪掉算法，該算法可以剪掉字符串中的任意字符或者代替字符串中的任意字符。
這樣的話，我們就可以將A∧B，□A，（A）全部替換為A，使用循環(huán)直到字符串的長度不再發(fā)生變化時循環(huán)結(jié)束，判斷其是否為一個單一命題變元。若是則返回TRUE值；若不是則返回FALSE值。
5.2 真值表生成 當(dāng)我們?nèi)藶榈脑诩埳蠘?gòu)造真值表時，只需要先列出原始命題變元及拆分出的命題公式，通過自己的計算依次填入真值即可，問題是如何在計算機(jī)上實(shí)現(xiàn)這一系列過程真值表前N列是N個原始的命題變元，我們?yōu)榱说玫秸麄€公式的，需要一點(diǎn)點(diǎn)將其化簡，即將類似“□P”，“PVQ”，“（P）”之類的命題公式化簡成為“P”，同時應(yīng)用公式中的符號和命題變元，首先識別符號讓計算機(jī)知道這個公式是做合取，析取，取反，條件還是雙條件，再根據(jù)公式中的命題變元計算出該公式對應(yīng)的真值存入真值表，記錄為一個新的命題變元而非公式，如此反復(fù)，直到最終整個原始公式只剩下一個命題變元，這個命題變元即為所求公式的真值。
本系統(tǒng)為了節(jié)省硬盤空間，以及提高效率，直接使用了arraylist數(shù)組代替在數(shù)據(jù)庫中建表實(shí)現(xiàn)真值表的生成，我將arraylist定義成boolean型數(shù)組類型，這樣每個arraylist中的一個元素其實(shí)都是真值表中的一列，而且可以任意添加，有效控制數(shù)量和空間復(fù)雜程度，這個類就是對真值表的初始化，運(yùn)行后的結(jié)果就如同畫好了真值表表格并已填入初始的單一命題變元的初始真值，為隨后的主范式計算做準(zhǔn)備。
5.3 大小項的生成 在計算出了真值之后，利用真值即可得出大項與小項，只要提取出前面定義的arraylist的最后一組，那一組里存的正是命題公式的真值，在得出大小項后可以生主范式。在web上只需要寫上一個調(diào)用getString（）方法的語句即可打印出來。
這里的原理類似于公式識別，也是將命題公式想辦法化簡，不同的是，每化簡一次都要修改真值表，也就是說在原先的arraylist數(shù)組后面再加一個元素，如此一來最后得到的元素必定存儲著命題公式的真值，大小項隨即得出。
5.4 主范式生成 在有了大小項之后，根據(jù)真值表法即可得出主合取范式以及主析取范式，由于在計算過程中，使用的符號都是計算機(jī)中的符號而非離散數(shù)學(xué)專業(yè)符號，但是給用戶的答案必須是專業(yè)的，所以在生成主范式的同時，也要對符號進(jìn)行標(biāo)準(zhǔn)化轉(zhuǎn)化。