發(fā)布時間：2024-05-11 15:36

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

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

【學位級別】：碩士

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



本文編號：3970076