時態邏輯及其在決策系統中的應用第1頁，共25頁，2023年，2月20日，星期六

斷言推理1目錄

時態邏輯

2

SIDSS系統描述

3

系統實現4

總結

5第2頁，共25頁，2023年，2月20日，星期六

斷言推理1Pre→Post由這樣的斷言推理為核心組織的產生式系統在決策支持系統、專家系統中使用得最多，也是最為成熟的解決方案但是語義是靜態的當遇到諸如動態的、實時的、并發的或具有其他時態特性的推理時，這種靜態的推理方式則有很大的缺陷時態邏輯斷言推理則可有效地彌補這方面出現的難題。第3頁，共25頁，2023年，2月20日，星期六

時態邏輯2時態邏輯（tenselogic）是非經典邏輯的分支學科其研究對象是:

把含有時態動詞的語句形式化

把含有這種語句的推理系統化引入以下常見的時態邏輯操作符：

Next:

ΟA,IfAandBareformulaethenΟA

Always:

□A,AlwaysinthefutureA

Sometimes:

A,SometimesinthefutureA

Until:

AUB,AuntilB

Since:

ASB,AsinceB

After:

AΠB,BafterA第4頁，共25頁，2023年，2月20日，星期六

系統描述3智能工資決策支持系統（SIDSS）是由劉冬寧、湯庸等人自主開發的一個典型的時態信息系統目前已有6000多家機關事業單位用戶針對我國機關事業單位工資政策復雜性、地域性和時間性等主要特點應用時態數據和知識處理技術解決了根據機關事業單位工作人員隨時間變化影響工資變動的信息（時態性數據），依據相應時期的工資政策（時態知識庫）自動確定工資的問題第5頁，共25頁，2023年，2月20日，星期六3.1SIDSS中的時態特征根據我國國情，工資政策繁雜，隨時間變動大在復雜的規則、高時態信息變動的條件下如何確保工資確定的正確性成了SIDSS中的重點和難點涉及到了大量的斷言推理與時態信息處理

系統描述3第6頁，共25頁，2023年，2月20日，星期六簡單地以工資政策中“兩年優秀晉升”的政策為例該政策在1999年以前的描述是這樣的：

如果人員連續兩年考核優秀，或某年考核優秀有“一年優”標志，工資檔次允許晉升一檔，考核結果有效年份從下年算起，但連續兩次晉升之間必須相隔兩年以上。在1999年以后的描述則改為：

其他與之前相同，但連續兩次晉升之間必須相隔四年以上。舉例說明：

人員A從1995年到2000年的考核均為優秀，則他可以分別在1997年和1999年執行一次工資檔次晉升，而不允許在2001年執行檔次晉升，正是由于1999年以后的工資政策規定，2001年與1999年之間并未相隔4年以上，因此不能進行晉升

系統描述3第7頁，共25頁，2023年，2月20日，星期六表1人員A工資晉升隨時間的變化年份考核結果執行操作政策依據1995優秀

1999年以前的“兩年優晉升”相隔必須兩年以上1996優秀1997年允許晉升一檔1997優秀

1998優秀1999年允許晉升一檔1999優秀

1999年以后的“兩年優晉升”相隔必須四年以上2000優秀2001年不允許晉升一檔

系統描述3第8頁，共25頁，2023年，2月20日，星期六3.2規則描述在“人員越級晉升”的過程中，會遇到的各種規則本文中僅以1999年更改政策一項規則變更為基準其規則、條件、動作的相關表如下：

系統描述3第9頁，共25頁，2023年，2月20日，星期六規則規則名規則說明起始條件表達式規則生命周期R1越級晉升用于處理1999年以前考核結果引起的越級晉升C1[1993/10,1998/12]R2越級晉升用于處理1999年以后考核結果引起的越級晉升C2[1999/1,NOW]表2越級晉升規則表

系統描述3第10頁，共25頁，2023年，2月20日，星期六表3越級晉升條件表條件條件THENELSEC1連續兩年考核結果優秀C3NULLC2連續兩年考核結果優秀C4NULLC3當前年份—上次越級晉升年份>=2或以前從未越級晉升A1NULLC4當前年份—上次越級晉升年份>=4或以前從未越級晉升A1NULL

系統描述3第11頁，共25頁，2023年，2月20日，星期六表4越級晉升動作表動作動作NEXTA1人員工資檔次加一檔NULL表2~4中，是關于“越級晉升”這一事件涉及到的規則、條件和動作。從表中可以看到這樣的規則、條件、動作具有斷言推理的特征，而其中在規則表中，定義的生命周期，更體現了時態變更性的特點，同時這一系列的判斷推理都具有強時序性，鑒于對推理的正確性應引入時態邏輯斷言推理。

系統描述3第12頁，共25頁，2023年，2月20日，星期六4.1時態邏輯斷言規則的設計根據表2~4，設計執行規則如下：（S1）WhenReceivePromotingApplication

Then_DoTimeVerificationAnd_ThenCondictionChecking（S2）WhenCondictionChecking

Then_DoPromotionExecuting在執行規則中體現出了較強的時間序列性（1）接到越級晉升的請求后，先判斷系統時間，根據規則的生命周期挑出該使用的條件序列判斷；（2）完成匹配條件序列判斷嵌套；（3）執行動作。

系統實現4第13頁，共25頁，2023年，2月20日，星期六進一步細化這些執行序列：（S3）WhenCondictionChecking

IfInvalidCondiction

Then_DoNext_CondictionChecking

UntilEndofLayer_CondictionChecking在條件判斷嵌套過程中，當前條件得不到匹配時，則輪轉到下一條件進行匹配，直到該層所有條件判斷完畢即判斷嵌套完成

系統實現4第14頁，共25頁，2023年，2月20日，星期六（S4）WhenCondictionChecking

IfEndofLayer_CondictionChecking

Then_DoRejectPromotingApplication在條件判斷嵌套過程中，當前條件得不到匹配和該層所有條件又判斷完畢時，則表示不符合越級晉升的條件，不通過該處理（S5）WhenNotInvalidCondiction

Then_DoNextLayer_CondictionCheckingUntilEndofAll_CondictionCheckingAnd_ThenPromotionExecute在條件判斷嵌套中，當前條件匹配成功則遞進到下一層條件判斷，如所有條件沒有判斷完畢則繼續進行判斷嵌套直到嵌套完畢，如嵌套完畢而條件匹配又成功則執行晉升動作

系統實現4第15頁，共25頁，2023年，2月20日，星期六4.2對斷言規則的邏輯描述對（S1）、（S2）邏輯描述如下：（S6）receive(SIDSS,Promoting_Application)=>verify(SIDSS,System_Time)Πcheck(SIDSS,Condiction)其中“Π”表示After，AΠB，意為BafterA。（S7）check(SIDSS,Condiction)=>act(SIDSS,Promotion)

系統實現4第16頁，共25頁，2023年，2月20日，星期六對（S3）-（S5）邏輯描述如下：（S8）check(SIDSS,Condiction)∧┑match(SIDSS,Condiction)=>samelayer_check(SIDSS,Condiction)Uend_check(Condiction,Layer)其中“U”在這里代表Until。（S9）┑match(SIDSS,Condiction)Πend_check(Condiction,Layer)=>reject(SIDSS,Promoting_Application)（S10）match(SIDSS,Condiction)=>(nextlayer_check(SIDSS,Condiction)Uend_check(Condiction,All))Πact(SIDSS,Promotion)

系統實現4第17頁，共25頁，2023年，2月20日，星期六4.3對規則生命周期的時態邏輯表示不僅可以對推理規則進行時態邏輯斷言設計以及邏輯推理，還可對規則的生命周期也用時態邏輯進行擴展。引入時態因子Ti時態因子狀態T1表示時間T2表示時間表5時態因子表

系統實現4第18頁，共25頁，2023年，2月20日，星期六因此對規則R1和R2的表示分別為：（1）AlwaysR1SinceT1UntilT2（2）AlwaysR2SinceT2用時態邏輯運算符表示為：（1）□((R1ST1)UT2)（2）□(R2ST1)

系統實現4第19頁，共25頁，2023年，2月20日，星期六4.4Java實現根據上述時態邏輯斷言，可以在代碼中實現上述規則斷言。調用TimeRoverInc.的TemporalRover工具它是一種用于處理Java程序中時態邏輯斷言并根據斷言生成有效Java代碼的工具，并可以配備數據庫表的工具DBRover同時使用。

系統實現4第20頁，共25頁，2023年，2月20日，星期六給出斷言規則（S6）-（S7）的Java偽代碼如下所示：S6:receivePromoting_Applicationimplies{Next{{checkCondiction}Until{verifySystemTime}}};S7:Always{{matchCondiction}implies{Next{actPromotion}}};

系統實現4第21頁，共25頁，2023年，2月20日，星期六給出斷言規則（S8）~（S10）的Java偽代碼如下所示：S8:If!{matchCondiction}implies{Next{{checkNext_Condiction}UntilEmpty{CondictionofthisLayer}}};S9:IfEmpty{CondictionofthisLayer}implies{Next!{actPromotion}};S10:If{matchCondiction}implies{Next{{{checkNextLayor_Condiction}UntilEmpty{AllCondictions}}implies{Next{actPromotion}}};

系統實現4第22頁，共25頁，2023年，2月20日，星期六對時態規則生命周期：（1）□((R1ST1)UT2)（2）□(R2ST1)給出Java偽代碼如下所示：（1）Always{{

R1SinceT1

}UntilT2

};（2）Always{

R2SinceT1

};