本文選題：非正規(guī)時(shí)態(tài)邏輯　切入點(diǎn)：矢列式系統(tǒng)　出處：《西南大學(xué)》2017年博士論文

【摘要】：時(shí)態(tài)邏輯是模態(tài)邏輯的一個(gè)重要分支。隨著人工智能、軟件工程、模型檢測(cè)等領(lǐng)域的產(chǎn)生和發(fā)展,時(shí)態(tài)邏輯在計(jì)算機(jī)科中越來(lái)越重要。本文研究的對(duì)象是極小非正規(guī)時(shí)態(tài)邏輯C2t,該邏輯是對(duì)E.J.Lemmon提出的極小非正規(guī)模態(tài)邏輯C2時(shí)態(tài)化處理后得到的。針對(duì)極小非正規(guī)時(shí)態(tài)邏輯C2t,本文從證明論、模型論和代數(shù)的角度開(kāi)展了以下5個(gè)方面的創(chuàng)新性工作:1.建立C2t的希爾伯特式公理系統(tǒng)HC2t。首先給出了C2t的語(yǔ)言和語(yǔ)義,C2t的語(yǔ)言和極小正規(guī)時(shí)態(tài)邏輯Kt的語(yǔ)言是相同的,但是在正則模型進(jìn)行解釋的。正則模型是非正規(guī)模態(tài)邏輯的模型,這種模型的特點(diǎn)在于模型中可以包含非正規(guī)世界。然后定義了公式在正則模型上的世界上是真的概念,與經(jīng)典模態(tài)邏輯不同的是:一個(gè)模態(tài)公式在某個(gè)世界上的真值不僅僅依賴(lài)于與該世界可及的其他世界上的信息,并且還依賴(lài)于該世界是否是正規(guī)世界。最后給出了HC2t的公理和推理規(guī)則,構(gòu)造了HC2t的典范模型,并利用典范模型證明了HC2t的完全性。2.建立C2t的加標(biāo)矢列式演算系統(tǒng)GC2t。加標(biāo)矢列式系統(tǒng)是近年來(lái)出現(xiàn)的一種證明系統(tǒng),其特點(diǎn)是將模態(tài)算子的語(yǔ)義改寫(xiě)成自然演繹規(guī)則,然后從自然演繹系統(tǒng)轉(zhuǎn)化為矢列式系統(tǒng)。首先定義矢列式的概念,建立GC2t的公理和推理規(guī)則。推理規(guī)則包括命題聯(lián)接詞規(guī)則、時(shí)序算子規(guī)則和關(guān)系規(guī)則。其次,證明了一些結(jié)構(gòu)規(guī)則在GC2t中是可允許的,例如弱化規(guī)則、收縮規(guī)則和切割規(guī)則,其中最重要的結(jié)構(gòu)規(guī)則是切割規(guī)則(cut rule)。然后,定義了正則模型的加標(biāo)擴(kuò)張,并證明GC2t(相對(duì)于正則模型的加標(biāo)擴(kuò)張)是可靠的和完全性。最后,證明了GC2t中的推導(dǎo)的可判定性。3.建立正則模型類(lèi)在時(shí)態(tài)語(yǔ)言下可定義的刻畫(huà)定理�？啥x性是模型論的核心問(wèn)題,它是研究模型類(lèi)或模型的性質(zhì)在一個(gè)邏輯語(yǔ)言中可定義或可表達(dá)的問(wèn)題。首先定義了正則模型上的一些關(guān)系,例如時(shí)態(tài)等價(jià)關(guān)系、同態(tài)、強(qiáng)同態(tài)和有界態(tài)射等。證明了滿足關(guān)系在強(qiáng)同態(tài)和有界態(tài)射下是保持不變的。其次定義了C2t-互模擬的概念,證明了滿足關(guān)系在C2t-互模擬下是保持不變的。定義了“C2t-像有窮”(C2t-image finite)的概念,證明了如果兩個(gè)正則模型是C2t-像有窮的,那么這兩個(gè)正則模型上的時(shí)態(tài)等價(jià)關(guān)系和C2t-互模擬關(guān)系是相等的。然后定義了正則模型的不相交并、生成子模型等概念,并證明了如果一個(gè)正則模型類(lèi)是時(shí)態(tài)可定義的,那么它在滿C2t-互模擬像,不相交并、生成子模型等運(yùn)算下是封閉的。定義了時(shí)態(tài)飽和的概念,并證明在時(shí)態(tài)飽和的正則模型類(lèi)上,時(shí)態(tài)等價(jià)蘊(yùn)含C2t-互模擬。定義了正則模型的C2t-超濾擴(kuò)張,證明了任何正則模型的C2t-超濾擴(kuò)張都是時(shí)態(tài)飽和的,并且時(shí)態(tài)可定義的正則模型類(lèi)在C2t-超濾擴(kuò)張下封閉。最后,證明了一個(gè)正則模型類(lèi)是時(shí)態(tài)可定義的當(dāng)且僅當(dāng)它在不相交并、滿C2t-互模擬像、C2t-超濾擴(kuò)張下是封閉的,并且它的補(bǔ)類(lèi)在C2t-超濾擴(kuò)張下也是封閉的。該刻畫(huà)定理解釋了時(shí)態(tài)語(yǔ)言在正則模型類(lèi)上的表達(dá)力。4.建立C2t語(yǔ)言與一階語(yǔ)言的對(duì)應(yīng)理論和C2t語(yǔ)言的有窮模型性。首先定義了C2t語(yǔ)言的標(biāo)準(zhǔn)翻譯,并證明了任意時(shí)態(tài)公式和其在標(biāo)準(zhǔn)翻譯下的一階公式是等值的。同時(shí),利用標(biāo)準(zhǔn)翻譯證明了C2t語(yǔ)言的緊致性。其次定義了正則模型的過(guò)濾的概念,并證明對(duì)任意正則模型和任意滿足一定條件的公式集,正則模型通過(guò)公式集的過(guò)濾總是存在的。最后,利用過(guò)濾的方法證明了C2t語(yǔ)言具有有窮模型性。5.建立C2t的代數(shù)語(yǔ)義學(xué)。首先定義了正則時(shí)態(tài)代數(shù),證明了正則時(shí)態(tài)代數(shù)的一些基本性質(zhì)。定義了正則框架的復(fù)代數(shù),并證明任意正則框架的復(fù)代數(shù)是一個(gè)正則時(shí)態(tài)代數(shù)。這表明從正則框架可以構(gòu)造出一個(gè)正則時(shí)態(tài)代數(shù)。其次定義了一個(gè)等式在正則時(shí)態(tài)代數(shù)上是真的概念,證明了一個(gè)等式在正則框架的復(fù)代數(shù)上是真的當(dāng)且僅當(dāng)該等式對(duì)應(yīng)的時(shí)態(tài)公式在正則框架上是有效的。然后,定義了C2t的林登博姆-塔斯基代數(shù)(Lindenbaum-Tarski Algebra),證明了它是正則時(shí)態(tài)代數(shù),在某種意義上,它是一種“典范的”正則時(shí)態(tài)代數(shù),即證明了C2t的定理所對(duì)應(yīng)的等式都在C2t的林登博姆-塔斯基代數(shù)上是真的。反之,在林登博姆-塔斯基代數(shù)上是真的等式所對(duì)應(yīng)的時(shí)態(tài)公式都是C2t的定理。利用上述結(jié)果,證明了C2t(相對(duì)于正則時(shí)態(tài)代數(shù))的代數(shù)完全性。最后,建立了正則時(shí)態(tài)代數(shù)的一個(gè)表示定理。具體來(lái)說(shuō),定義正則時(shí)態(tài)代數(shù)的超濾框架,并證明任意正則時(shí)態(tài)代數(shù)都可以嵌入到它的超濾框架的復(fù)代數(shù)上,同時(shí)證明了C2t的典范框架和和它的林登保姆-塔斯基代數(shù)的超濾框架是同構(gòu)的。本文開(kāi)展的上述工作,從理論上豐富了現(xiàn)有的時(shí)態(tài)邏輯系統(tǒng),并建立了一些重要的結(jié)論。這些結(jié)論在軟件規(guī)約、自動(dòng)定理證明和模型檢測(cè)等方面都有一定的指導(dǎo)意義。因此本文的研究,不僅具有理論意義,而且具有應(yīng)用價(jià)值。
[Abstract]:......
【學(xué)位授予單位】：西南大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2017
【分類(lèi)號(hào)】：B81

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 周文華;;基于區(qū)間的三值時(shí)態(tài)邏輯[J];湖北社會(huì)科學(xué);2009年03期

2 劉虎;;開(kāi)放系統(tǒng)中智能體競(jìng)爭(zhēng)的時(shí)態(tài)邏輯[J];中山大學(xué)學(xué)報(bào)(社會(huì)科學(xué)版);2008年02期

3 王輝;;混合語(yǔ)言與時(shí)態(tài)邏輯[J];湖南科技大學(xué)學(xué)報(bào)(社會(huì)科學(xué)版);2009年02期

4 張家龍;;略談時(shí)態(tài)邏輯[J];國(guó)內(nèi)哲學(xué)動(dòng)態(tài);1979年12期

5 馮彥波;;論時(shí)態(tài)邏輯的新發(fā)展[J];鄭州航空工業(yè)管理學(xué)院學(xué)報(bào)(社會(huì)科學(xué)版);2008年04期

6 白金山;李祥;;具有自反性質(zhì)的線序時(shí)態(tài)邏輯研究[J];計(jì)算機(jī)工程與設(shè)計(jì);2011年04期

7 杜國(guó)平;;知識(shí)蘊(yùn)涵時(shí)態(tài)邏輯系統(tǒng)[J];安徽大學(xué)學(xué)報(bào)(哲學(xué)社會(huì)科學(xué)版);2009年05期

8 唐同誥;;程序算子與邏輯算子的統(tǒng)一——一階時(shí)態(tài)邏輯(關(guān)系邏輯)[J];貴州大學(xué)學(xué)報(bào)(自然科學(xué)版);1986年03期

9 馮彥波;;決定論、邏輯決定論與時(shí)態(tài)邏輯[J];內(nèi)蒙古農(nóng)業(yè)大學(xué)學(xué)報(bào)(社會(huì)科學(xué)版);2008年01期

10 吳新民;;時(shí)態(tài)邏輯與時(shí)間思想的語(yǔ)言哲學(xué)維度[J];湖南社會(huì)科學(xué);2011年04期

相關(guān)會(huì)議論文 前5條

1 田國(guó)會(huì);劉長(zhǎng)有;徐心和;;離散事件動(dòng)態(tài)系統(tǒng)理論的時(shí)態(tài)邏輯研究方法[A];1996中國(guó)控制與決策學(xué)術(shù)年會(huì)論文集[C];1996年

2 田國(guó)會(huì);劉長(zhǎng)有;徐心和;;電梯服務(wù)系統(tǒng)的時(shí)態(tài)邏輯描述、分析與控制[A];1996年中國(guó)控制會(huì)議論文集[C];1996年

3 陳玉泉;陳宣;陸汝占;;內(nèi)涵時(shí)態(tài)邏輯的語(yǔ)義解釋系統(tǒng)[A];自然語(yǔ)言理解與機(jī)器翻譯——全國(guó)第六屆計(jì)算語(yǔ)言學(xué)聯(lián)合學(xué)術(shù)會(huì)議論文集[C];2001年

4 李曉鷗;郭令忠;徐心和;;Petri網(wǎng)監(jiān)控的時(shí)態(tài)邏輯框架[A];1994中國(guó)控制與決策學(xué)術(shù)年會(huì)論文集[C];1994年

5 劉新;鄒麗;;直覺(jué)模糊時(shí)態(tài)邏輯[A];模糊集理論與應(yīng)用——98年中國(guó)模糊數(shù)學(xué)與模糊系統(tǒng)委員會(huì)第九屆年會(huì)論文選集[C];1998年

相關(guān)博士學(xué)位論文 前2條

1 王善俠;極小非正規(guī)時(shí)態(tài)邏輯研究[D];西南大學(xué);2017年

2 呂嘉;基于開(kāi)放時(shí)態(tài)邏輯的面向方面程序形式化驗(yàn)證和模塊推理研究[D];浙江大學(xué);2009年

相關(guān)碩士學(xué)位論文 前8條

1 田潔;基于時(shí)態(tài)邏輯的管制員響應(yīng)執(zhí)行差錯(cuò)建模與分析方法研究[D];中國(guó)民航大學(xué);2016年

2 劉冬寧;時(shí)態(tài)邏輯及其對(duì)知識(shí)庫(kù)的構(gòu)架與研究[D];廣東工業(yè)大學(xué);2004年

3 李嵐;略論時(shí)態(tài)邏輯在計(jì)算機(jī)科學(xué)中的發(fā)展[D];華東師范大學(xué);2013年

4 李學(xué)軍;基于時(shí)態(tài)邏輯的遷移實(shí)例運(yùn)行時(shí)安全研究[D];山東大學(xué);2009年

5 王勝;基于SystemC的時(shí)態(tài)邏輯屬性驗(yàn)證方法研究[D];北京化工大學(xué);2009年

6 趙峗;基于時(shí)態(tài)邏輯的UML交互模型檢測(cè)研究[D];青島大學(xué);2008年

7 白金山;二元判斷圖BDD及其JAVA實(shí)現(xiàn)的應(yīng)用與研究[D];貴州大學(xué);2008年

8 張紅軍;一類(lèi)對(duì)象Petri網(wǎng)建模與驗(yàn)證方法研究[D];鄭州大學(xué);2006年

，

本文編號(hào)：1669646