中間邏輯中的范式研究.pdf

1、中間邏輯是強(qiáng)弱介于經(jīng)典邏輯與直覺(jué)主義邏輯之間的一大類命題邏輯。近年來(lái)，這些邏輯在計(jì)算機(jī)科學(xué)領(lǐng)域中受到極大的重視。而范式在邏輯及其相關(guān)領(lǐng)域中起著很重要的作用，特別是對(duì)于自動(dòng)定理證明、自動(dòng)推理和邏輯程序領(lǐng)域。本論文的主要目的是：尋找一些可以應(yīng)用到基于中間邏輯的自動(dòng)定理證明、自動(dòng)推理和邏輯程序等領(lǐng)域的有用范式；研究這些范式在各中間邏輯中的存在性；設(shè)計(jì)一些用來(lái)對(duì)公式進(jìn)行以上范式化簡(jiǎn)的算法。 在本論文中，我們深入地研究了中間邏輯中的范式問(wèn)

2、題。共涉及到六種范式，包括：蘊(yùn)含范式、擴(kuò)展合取與析取范式、弱合取、析取與蘊(yùn)含范式。我們證明了HT邏輯是唯一的具有蘊(yùn)含范式的非經(jīng)典中間邏輯，同時(shí)研究了三種弱范式在Gdel邏輯中的存在性。對(duì)于公式的范式化簡(jiǎn)，我們提出了兩類范式化簡(jiǎn)算法，一類是基于模型刻畫(huà)公式的語(yǔ)義方法，另一類是基于重寫(xiě)系統(tǒng)的語(yǔ)法方法。作為以上研究的附加結(jié)果，我們得到了四種模型刻畫(huà)公式，引入了Kripke模型之間初等蘊(yùn)含的概念，并給出了一個(gè)初等蘊(yùn)含的充分必要條件。最后