本文在研究了命題投影時(shí)序邏輯PPTL(Propositional Projection Temporal Logic)的語義和語法的基礎(chǔ)上,詳細(xì)闡述了它的判定過程和表達(dá)性。首先介紹了命題投影時(shí)序邏輯,包括基本的語法、語義和一些派生公式及常用邏輯等式,該邏輯除了包含有常用的邏輯操作符∨(或)和?(非)外,還包含了兩個(gè)時(shí)序操作符○(next)和prj(投影操作符)。其次,本文定義了命題投影時(shí)序邏輯公式的正則形(normal form),根據(jù)公式的結(jié)構(gòu)采用歸納的方法證明了任意PPTL公式都可以轉(zhuǎn)換為正則形定理的正確性并且給出了相應(yīng)的轉(zhuǎn)換算法。該算法將所有邏輯公式都?xì)w結(jié)為一種統(tǒng)一的形式,這是采用Tableau方法進(jìn)行判定的前提和基礎(chǔ)。再次,為了找到給定公式的模型,本文介紹了正則圖(normal form graph)的概念,給出了為PPTL公式構(gòu)造正則圖的算法和命題投影時(shí)序邏輯的判定過程,該方法簡單實(shí)用。最后,本文介紹和比較了區(qū)間時(shí)序邏輯中兩個(gè)版本的投影結(jié)構(gòu)并研究了這兩個(gè)投影結(jié)構(gòu)的表達(dá)性,結(jié)果表明prj投影結(jié)構(gòu)比原始的投影結(jié)構(gòu)proj的表達(dá)性更強(qiáng)。

【文章頁數(shù)】：70 頁

【學(xué)位級(jí)別】：碩士

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 引言
    1.2 時(shí)序邏輯
    1.3 相關(guān)工作
    1.4 論文的研究意義和目的
    1.5 論文的主要工作
第二章 命題投影時(shí)序邏輯
    2.1 語法
    2.2 語義
        2.2.1 狀態(tài)
        2.2.2 區(qū)間
        2.2.3 解釋
    2.3 聯(lián)結(jié)詞的擴(kuò)充
    2.4 可滿足性和有效性
        2.4.1 可滿足性和有效性
        2.4.2 特殊模型
    2.5 優(yōu)先級(jí)
    2.6 邏輯定理
    2.7 本章小結(jié)
第三章 命題投影時(shí)序邏輯的正則形
    3.1 命題投影時(shí)序邏輯的正則形
    3.2 命題投影時(shí)序邏輯公式轉(zhuǎn)換為正則形的算法
    3.3 本章小結(jié)
第四章 命題投影時(shí)序邏輯的可判定性
    4.1 正則圖
    4.2 判定算法
    4.3 判定算法優(yōu)越性的討論和比較
    4.4 本章小結(jié)
第五章 命題投影時(shí)序邏輯的表達(dá)性
    5.1 兩個(gè)投影結(jié)構(gòu)
        5.1.1 投影結(jié)構(gòu)prj
        5.1.2 投影結(jié)構(gòu)proj
    5.2 兩個(gè)投影結(jié)構(gòu)的比較
        5.2.1 使用新投影結(jié)構(gòu)prj 表示原始投影結(jié)構(gòu)proj
        5.2.2 使用投影結(jié)構(gòu)proj 和chop 結(jié)構(gòu);來推導(dǎo)投影結(jié)構(gòu)prj
        5.2.3 投影結(jié)構(gòu)proj 和chop 結(jié)構(gòu)的關(guān)系
    5.3 本章小結(jié)
第六章 結(jié)論
    6.1 總結(jié)
    6.2 展望
致謝
參考文獻(xiàn)
作者在讀期間的研究成果



本文編號(hào)：3970076