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

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