命題模態邏輯S5系統中并行推理方法*

楊 洋，李廣力，張桐搏，劉 磊，呂 帥,2,3+

1.吉林大學 計算機科學與技術學院，長春 130012

2.吉林大學 數學學院，長春 130012

3.符號計算與知識工程教育部重點實驗室（吉林大學），長春 130012

命題模態邏輯S5系統中并行推理方法*

楊 洋1，李廣力1，張桐搏1，劉 磊1，呂 帥1,2,3+

1.吉林大學 計算機科學與技術學院，長春 130012

2.吉林大學 數學學院，長春 130012

3.符號計算與知識工程教育部重點實驗室（吉林大學），長春 130012

YANG Yang,LI Guangli,ZHANG Tongbo,et al.Parallel reasoning methods in propositional modal logic S5. Journal of Frontiers of Computer Science and Technology,2016,10(12)：1783-1792.

S5系統是一類知識表示能力和處理能力都較強的模態公理系統，它是認知邏輯、信念邏輯等非經典邏輯理論的基礎。根據Kripke語義模型以及S5系統中部分公理，對命題模態邏輯S5公理系統的性質進行了較為深入的研究，并對S5系統中一類具有代表性的標準模態子句集的特性進行了分析，提出了一種基于擴展規則方法的命題模態邏輯推理算法（propositional modal clausal reasoning based on novel extension rule，PMCRNER）。針對樸素算法時間復雜度較高的問題，利用任務間潛在的關聯性對算法同時進行了粗粒度與細粒度并行化，提出了并行算法PPMCRNER（parallel PMCRNER）理論框架，并且與基本算法進行了對比。實驗結果表明，PPMCRNER算法在不可滿足的子句集上的推理具有良好的加速比，為高時間復雜性的模態推理方法的進一步研究提供了一種可行方案。

命題模態邏輯；S5公理系統；并行推理；擴展規則

1 引言

近年來，多種以模態邏輯為基礎的復雜公理系統與框架被相繼提出[1-3]，關于模態邏輯甚至是更高階的邏輯知識表示形式的理論研究逐漸成為人們關注的熱點[4]。模態邏輯推理方法的研究是高階公理系統和框架的原型實現的基礎。自動推理領域主流的推理方法為歸結方法、表推演方法和擴展規則推理方法。推理的公式集一般為非CNF（conjunctive normal form）和CNF公式。結合基礎推理方法，命題模態邏輯的推理方法有直接推理和轉換推理兩種。鑒于不同模態系統中的公理存在著較大差異，因此現階段主流模態推理方法和證明系統大部分都是基于具體的模態公理系統或者模態語言。

2006年，Wu等人提出了一種在命題模態邏輯K系統中的破壞性擴展規則推理方法[5]，并且將擴展規則推理過程和化簡過程交替進行，加速算法的求解過程。該方法保留了擴展規則求解問題的優勢，對于互補因子率較高的模態公式能夠快速地進行可滿足性判定。同年，Schmidt探討了命題動態模態邏輯不同推理方法的發展，闡明了表推演系統、歸結系統、雙重表推演系統中如何通過一些規則使其能夠擴展到一階命題邏輯[6]。2007年，Nalon等人提出了一種正規模態邏輯中基于歸結的推理方法，通過一組公理來對模態邏輯公式進行直接推理，同時為許多正規多模態邏輯的推理方法給出了正確性和完備性的結果[7]。2008年，吳瑕等人提出了一種命題模態邏輯中關系擴展規則推理方法[8]。其主要思想是使用關系轉換函數對Kripke語義模型進行轉換，使用一階擴展規則方法對轉換后的結果進行推理。2013年，Benzmüller等人提出了一種使用高階邏輯定理證明器來求解一階模態邏輯可滿足性問題的方法，并且給出了一階模態邏輯（first-order modal logic，FML）到高階邏輯（high-order logic，HOL）的轉換工具[9]。近年來，由于SAT（satisfiability）比賽的推廣以及命題邏輯SAT求解器求解效率的大幅提升，更多的學者開始尋求轉換方法來將多種不同的模態公理系統轉化為命題SAT求解。2013年，Kaminski等人通過一組公理轉換規則將模態可滿足性問題轉化成普通的布爾可滿足性問題，調用命題SAT求解器進行求解，得到了較好的效果[10]。2014年，Rajeev等人提出了一種使用二元決策圖（binary decision diagrams，BDDs）替換DPLL的算法求解模式來求解模態可滿足性問題，通過與多個求解器進行對比展現了其優越的求解能力[11]。

2 基礎知識

2.1 擴展規則

擴展規則方法的原理為給定命題變量集上的所有極大項之間的合取是不可滿足的。擴展規則[12]的定義為：給定一個子句C和不在C中出現的原子a，D={C∨a，C∨?a}，稱由C到D的推導過程為擴展規則，D為子句C關于原子a應用擴展規則的結果。顯然，公式集D在真值指派上和公式集C邏輯等價。因此，可以對子句集中的任意子句應用類似上述的推導過程，逐步擴展成只包含形式為極大項的子句集。樸素擴展規則算法（extension rule，ER）的基本思想是：搜索所有的極大項空間，若待判定的子句集能夠擴展出所有的極大項空間，則該子句集不可滿足；否則該子句集可滿足。

在2009年李瑩等人提出的基于擴展規則的NER（novel extension rule）推理方法中[13]，其進行逆向推理，不斷取給定命題變量集上的極大項依次判斷能否被指定子句集擴展出來，以此來獲得公式是否可滿足的結論。在該方法中，其避免了樸素擴展規則ER繁重的容斥原理求解過程和內存溢出問題，以時間效率換取空間開銷，是一種較優的推理方法。本文將借助NER推理方法來進行模態公式推理。

目前，擴展規則的應用研究還僅限于起步階段，其研究成果主要包括命題邏輯知識編譯、搜索方法的啟發式策略、可能性推理與知識編譯、模型計數以及#SAT問題求解等[14-19]。而對于高階邏輯的推理方法的應用研究還處于空白階段。

2.2 命題模態系統

命題模態邏輯公理系統在命題邏輯系統的基礎上進行了擴展，在保持系統推理結構封閉的情況下加入了部分公理和規則。公理系統分為正規系統和非正規系統，通常對模態邏輯的正規系統進行推理。常用的模態邏輯正規系統主要有K、T、D、S4、S5、B等系統。K系統為命題模態邏輯中最小的正規系統，它相比于經典命題邏輯系統增加了K公理(□(P→Q)→(□P→□Q))和必然化規則（如果?KP，則?K□P）。而其他系統分別在K系統的基礎上添加了相應的公理，使得相應的公理系統增加了不同的約束和性質。需要強調的是：S5系統是在T系統的基礎上添加了E公理而形成的[20]。命題模態邏輯推理是在特定的公理系統中對一組任意的命題模態公式進行可滿足性判斷的過程。命題模態邏輯推理的過程比命題邏輯推理更復雜，因為在對模態公式進行推理時不僅要考慮命題變量集的真值指派，還要考慮必然和可能算子導致的命題公式在Kripke可能世界模型中的世界轉移，所以如何對模態算子的處理是命題模態邏輯推理過程的核心，對于命題的部分，只需要考慮使用常規命題邏輯的推理方法即可。命題模態邏輯S5公理系統是一種有代表性的公理系統，它也是認知邏輯和信念邏輯的基礎。在S5系統中，可以只保留一個模態算子，即必然算子□。在不同的邏輯中，該算子代表的含義也不盡相同。如在認知邏輯中，該算子代表某智能體知道某個事件；而在信念邏輯中，該算子代表某個智能體相信某個事件。因此，研究該系統的推理方法對于更高級的認知邏輯、信念邏輯和道義邏輯等推理方法的研究有著重要意義。

需要指出的是，目前命題模態邏輯的推理方法研究還處于理論階段，并且大多數對于該邏輯的研究主要集中在K、T公理系統中，對于多約束的公理系統的通用形式化推理算法還較少，本文將對S5系統的推理方法進行研究，并進行一系列相關實驗。

3 命題模態邏輯S5系統中標準模態子句集推理方法

3.1 定義與引理

模態邏輯S5公理系統在T系統的基礎上增加了E公理（◇P→□◇P），利用該公理，對于系統中的模態公式可以進行模態度歸約，使得任意公式能夠歸約為模態度小于等于1的模態公式，并且通過化簡等手段將模態公式轉化為標準模態子句集或者標準模態子句塊。

下面給出標準模態子句的定義：

標準模態子句：令ФP為模態文字，其中Ф是有限個必然與可能算子的序列，并且該序列可以為空串，P為命題文字。若干個模態文字的析取式為標準模態子句。

S5系統具有對稱性，不能使用破壞性方法對其進行推理，因此可以通過間接轉化的方法對其進行推理，其中最重要的轉化規則為分裂規則和歸約規則。

分裂規則[5]：如果一個子句集包含一個至少包含兩個模態文字的子句C，那么該子句集可以由兩個子句集來替代，其中一個子句集是原子句集中非C子句集與子句C中的一個模態文字的合取，另一個子句集是原子句集中非C子句集與子句C中的其余子句的合取。

歸約規則：因為S5系統是S4系統的擴張，那么借助S4系統中與S5系統中□P?□□P，◇P?◇◇P，◇P?□◇P，□P?◇□P這4條定理，可以對任意長度的模態算子序列，刪去前面的任意長度而只保留最里層的模態算子。

因為K系統是最小的正規模態系統，所以K系統中的任意定理在S5系統中都適用，K系統中的定理(◇P∨◇Q?◇(P∨Q))可以應用于S5系統中，對在一個標準模態子句中具有相同可能算子前綴的模態文字進行合并，便于后續處理。

單模態單元子句：令ФQ為單模態單元子句，其中Ф是單個必然算子或者單個可能算子或者為空，Q為命題邏輯中的標準子句。由單模態單元子句組成的子句集叫作單模態單元子句集。

3.2 基于NER的命題模態子句推理算法

基于上述的規則和定義，命題模態邏輯S5系統中子句形式的推理算法的核心思想如下：

（1）預處理

對于初始輸入的標準模態子句集，使用歸約規則對含有超過一個模態算子序列的模態文字進行歸約，使得算法真正處理的輸入為所有模態文字均不含有超過一個模態算子的標準模態子句集，該操作能夠在線性時間復雜度內完成。

（2）合并

掃描經過預處理的標準模態子句集，對子句中出現的形如◇P∨◇Q析取式進行合并。注意，形如□P∨□Q的公式無法進行合并，因為合并后的形式與原形式不保持Kripke語義等價，只合并可能算子。該操作同樣能夠在線性時間復雜度內完成。

（3）拆分

任意選取經過合并操作后的子句集中的非單模態單元子句，使用分裂規則對子句集進行拆分，形成兩個子句列表，子句列表之間的可滿足性為析取關系。

（4）可滿足性判定

在拆分過程中，可以邊拆分邊判斷，判斷的形式是拆分的子句列表出現單模態單元子句集。調用可滿足性判定算法（在后文詳述）。如果一個子句列表判定為可滿足，則結束全部的拆分和求解過程，返回可滿足；否則只有當所有子句列表都返回不可滿足時，算法結束。

單模態單元子句集的可滿足性判定：

輸入參數為單模態單元子句集時，考慮到多模態算子公式已經被歸約為單模態算子，則在處理單模態算子時只需要考慮一層的世界轉移即可，即判斷當前世界以及當前世界的后繼世界即可，不需要再考慮后繼的后繼或者更多，因此在處理過程中只需要將子句集轉化成命題形式即可。

對于命題子句集，不僅需要考慮當前世界的可滿足性，還得考慮其對后繼世界的可滿足性影響。因為S5系統是在T公理系統之上的模態邏輯公理系統，則T公理系統中的約束對于S5系統同樣成立。在T公理系統中，有公理P→◇P，則在處理單模態單元子句集時，需要將每一個出現的命題子句進行復制，并且對復制后的每一個子句最外層附加一個可能算子，將這樣的公式加入原單模態單元子句集中進行求解。對于帶模態算子的子句，優先考慮帶必然算子的單模態單元子句，當前世界的后繼世界的個數為命題變量個數的2的冪次方。在可滿足性判定時，首先使用該子句列表中的所有帶必然算子的單模態單元子句依次對這些不可滿足的后繼可能世界進行“殺死”操作，進行完一輪后，剩余的可能世界集為滿足所有帶必然算子中的命題公式。然后將帶可能算子的單模態單元子句的命題部分傳遞到剩余世界判定，如果存在一個世界能夠使得該子句的命題部分為真，則判斷結束，依次判斷所有帶可能算子的單模態單元子句。

開始使用帶必然算子的單模態單元子句集“殺死”任意一個使其命題部分為假的世界實際上是對于該部分子句集的命題部分，尋找是否有解，能夠使得帶必然算子的單模態單元子句的命題部分全部為真。接下來使用帶可能算子的單模態單元子句的命題部分在剩下的世界里尋找是否存在能夠使其為真的世界，是將每一個帶可能算子的單模態單元子句的命題部分加入帶必然算子的單模態單元子句集的命題部分尋找該整體命題子句集是否有解。最后對命題部分的求解，同樣是受限于T公理的約束，在T公理系統中，有公理（□P→P）。因此，必須將該子句列表中的所有帶必然算子的單模態單元子句的命題部分進行剝落，然后將其添加到該子句列表的命題公式部分，統一進行可滿足性判定。

因此本文在處理過程中將帶必然算子的單模態單元子句集的命題部分單獨判定其可滿足性，然后依次把帶可能算子的單模態單元子句的命題部分加入到帶必然算子的單模態單元子句集的命題子句集中，判定其可滿足性，只要存在一個使其不可滿足，則整體不可滿足，只有每一個帶可能算子的單模態單元子句判定均可滿足，則整體才可滿足。

例 F={□◇□A∨◇◇B,□?A∨◇?B∨C}，對該公式的推理步驟如下：

返回SAT。

綜上所述，給出命題模態邏輯S5中的子句形式的推理算法。

算法1 PMCRNER（propositional modal clausal reasoning based on novel extension rule）

算法2 SMRNER（single modal reasoning based on novel extension rule）

算法1中的IsSingle函數是判斷當前合取公式是否為單模態單元子句集，如果是，則調用基于NER的單模態單元子句集求解算法SMRNER進行求解，否則繼續進行拆分，直到所有單模態單元子句集全部被處理。choose函數是在公式F1中任意選擇一個標準模態子句進行拆分。

算法2中的GetP函數的功能為得到當前子句列表中的命題部分；AddPO函數的功能為為當前子句列表中的每一個命題子句的最外層添加一個可能算子，將其變成命題模態子句；GetNO函數的功能為得到當前子句列表中所有帶必然算子的子句的命題部分；GetPO函數的功能為得到當前子句列表中所有帶可能算子的子句的命題部分。

顯然，該算法對于命題模態邏輯S5公理系統中的子句形式推理是正確并且完備的。

3.3 PPMCRNER算法

上節給出了PMCRNER算法，但樸素版本的算法時間復雜度較高，需要尋找新的方法使得算法的執行效率得到提高，在進行可滿足性判定時能夠提前結束。本節將該形式的推理算法進行了并行化，在特定的子句集上得到了較好的加速效果。

3.3.1 粗粒度并行

上節中，將標準模態子句拆分成不同的子句列表進行求解，該部分在串行算法中是順序執行的。可以將該部分執行過程并行化，得到粗粒度并行的目的。

3.3.2 細粒度并行

也可以考慮將子句列表的可滿足性判定過程并行化。在對子句列表運用T系統中的兩條公理后，將后繼世界之間的可滿足性判定和命題邏輯的可滿足性判定并行化。由于多個帶可能算子的子句均需要同所有帶必然算子的子句進行后繼世界可滿足性判定，可以將它們的執行過程并行化，同時將命題部分的執行過程同樣并行化，達到細粒度并行的目的。

3.3.3PMCRNER算法的并行化

綜上所述，當將算法粗粒度和細粒度并行化之后，就得到了全并行的PMCRNER推理算法——PPMCRNER算法。下面給出PPMCRNER算法的理論框架。

在算法執行之前，需要對公式集進行預處理，處理的大致流程如下。

算法3 PPMCRNER(parallel propositional modal clausal reasoning based on novel extension rule)

否則返回第1步.

算法4 PSMRNER（parallel single modal reasoning based on novel extension rule）

在Predeal中，flag變量和Flag[]數組分別為標記變量和標記數組，用于主方法對子方法進行調度控制。在PPMCRNER算法中，Allocate函數的功能為將當前生成的單模態單元子句集（子句列表）按照一定的策略分給某個分方法，用于并行執行。算法中其余符號與PMCRNER算法中的符號含義相同。

4 實驗結果與分析

該部分擬采用隨機生成的標準模態子句集來對串行、全并行算法的性能進行測試。在進行實驗的過程中，發現同樣規模的標準模態子句集和命題邏輯子句集，在推理時其時間復雜度已經差了好幾個數量級。因此，為了實驗能夠產生令人接受的有效結果，在隨機生成標準模態子句集時將標準模態子句中的必然算子的個數限制在3個以內，而可能算子的個數與命題原子的個數不作限制。本文分別在可滿足的標準模態子句集和不可滿足的標準模態子句集上進行了大量的測試，隨機樣例有兩個參數＜N, K＞，其中N代表子句集中變量的個數，K代表子句的個數。實驗環境：Windows 8操作系統，i7-3770 CPU，8 GB RAM。

4.1 不可滿足子句集

本組對比實驗中，選取命題變量數為10，模態算子數任意的不可滿足標準模態子句集進行測試，結果如圖1所示。其中，圖（a）為串行算法和全并行算法的時間對比圖，橫軸為子句數，縱軸為CPU時間。圖（b）為全并行算法相對于串行算法的加速比。很明顯，隨著子句數的不斷增加，加速比呈不斷上升趨勢并且接近于3。

本組對比實驗中將命題變量數改為15，其余條件和設定同上組實驗一樣，結果如圖2所示。可以看出，該組對比實驗呈現出了與上組實驗相同的效果和趨勢。可以認為，該算法對于不同規模的測試樣例是具有穩定性的。

Fig.1 Experimental results of random problem＜10,K＞instances on unsatisfiable clause sets圖1 不可滿足子句集上隨機問題＜10,K＞用例測試結果

4.2 可滿足子句集

本組對比實驗里選取命題變量數為10，模態算子數任意的可滿足標準模態子句集進行測試，結果如圖3所示。其中，圖（a）為串行算法和全并行算法的時間對比圖，橫軸為子句數，縱軸為CPU時間。圖（b）為全并行算法相對于串行算法的加速比。可以看出，在測試數據為可滿足子句集的情況下，串行算法和全并行算法的效率差距不大，且略高于全并行算法。

同樣的，對于可滿足的標準模態子句集，增加測試數據的規模，將命題變量數增加到15，結果如圖4所示。可以看出，即使測試數據的規模增加，算法的對比結果仍然保持同樣的趨勢。算法對于可滿足的不同規模的測試數據是具有穩定性的。

Fig.2 Experimental results of random problem＜15,K＞instances on unsatisfiable clause sets圖2 不可滿足子句集上隨機問題＜15,K＞用例測試結果

4.3 分析

本文對大量數據集進行了測試，分析結果如下：

（1）此類測試數據集具有代表性的通用benchmark較少，故采用隨機生成的策略來產生數據集。大量測試表明，隨機生成可滿足的標準模態子句集更容易。

（2）模態公式的推理時間復雜度遠遠超過了同規模的命題公式，子句個數一旦過大，推理的時間復雜度將以指數級別的增長趨勢達到讓人難以接受的程度。

（3）從大量測試數據來看，并行算法具有一定的適用性。事實上，并行算法并不是在所有的標準模態子句集上都比串行快，相反的，在某些特定的子句集上其性能略低于串行算法。在可滿足的標準模態子句集上，并行算法的執行效率反而比串行算法慢。原因在于對可滿足的標準模態子句集進行推理的時候，大部分子句集在拆分子句列表的時候其中前一部分子句列表集合中就已經出現可滿足的子句列表，那么并行算法的粗粒度并行并沒有得到真正執行。相反的，并行算法真正實現的時候其復雜的線程之間的調度與通信往往是一筆不小的開銷，執行效率反而有所降低。

（4）并行算法對于不可滿足的標準模態子句集具有穩定的加速比，但無論分多少個任務并行，真正的加速比還是受限于CPU物理內核的個數，其加速比能夠接近CPU物理內核的個數。

（5）實驗表明，細粒度并行策略的加速比并不顯著。在實驗中，嘗試分別將粗粒度并行與細粒度并行進行分開實驗。事實上，全并行算法的加速比和只有粗粒度并行的版本相比，其加速程度并沒有明顯提高。細粒度并行的加速程度主要受限于單模態單元子句集中可能算子的個數，同時在粗粒度與細粒度同時并行的時候，其融合后的加速比受限于物理硬件。

Fig.3 Experimental results of random problem＜10,K＞instances on satisfiable clause sets圖3 可滿足子句集上隨機問題＜10,K＞用例測試結果

Fig.4 Experimental results of random problem＜15,K＞instances on satisfiable clause sets圖4 可滿足子句集上隨機問題＜15,K＞用例測試結果

5 結論與展望

本文提出了命題模態邏輯S5系統中一種新的基于擴展規則的標準模態子句集的串行推理算法和并行推理算法，并對其進行了大量的對比測試。實驗表明，PPMCRNER算法具有一定的適用性，在不可滿足的子句集中具有穩定的加速比，在可滿足的子句集中加速效果并不明顯。

完備算法的時間復雜度較高，原因在于一旦標準模態子句中必然算子的個數增加，則整個子句集的推理時間復雜度的增加程度是難以接受的。此外完備算法中應用規則時，標準模態子句中只有可能算子間的文字能夠進行合并，而必然算子間卻不允許，原因在于◇P∨◇Q?◇(P∨Q)成立，而□P∨□Q?□(P∨Q)卻不成立。因此可以在實際推理時先運行一個不完備的算法，思想是加強完備算法中的歸約規則，加入一條定理□P∨□Q→□(P∨Q)。運用此定理合并標準模態子句中的所有必然算子，將所有的標準模態子句全部變成最多只有一個必然算子和一個可能算子的子句，這樣推理的時間復雜度會大大降低。如果不完備算法返回不可滿足，則原公式也不可滿足；若不完備算法返回可滿足，則需要重新調用完備的算法來進行推理。

可以進一步研究并行算法的粗粒度并行策略，使得其對于可滿足的標準模態子句集也同樣具有穩定的加速比。該問題的關鍵在于采用何種子句列表拆分策略使得各分線程在能夠“均勻”地處理子句列表的同時，線程之間的同步與通信的開銷不至于過大，這樣可以使得算法的加速性能得到進一步提升。

[1]Meghdad G.Distributed knowledge justification logics[J]. Theory of Computing Systems,2014,55(1):1-40.

[2]Zadeh L A.A note on modal logic and possibility theory[J]. Information Sciences,2014,279:908-913.

[3]Larsen K G,Mardare R.Complete proof systems for weighted modal logic[J].Theoretical Computer Science,2014,546: 164-175.

[4]French T,van der Hoek W,Iliev P,et al.On the succinctness of some modal logics[J].Artificial Intelligence,2013, 197:56-85.

[5]Wu Xia,Sun Jigui.Destructive extension rule in proposition modal logic K[C]//Proceedings of the 1st International Conference on Computational Methods,Singapore,Dec 15-17,2004:1087-1091.

[6]Schmidt R A.Developing modal tableaux and resolution methods via first-order resolution[C]//Proceedings of the 6th Conference on Advances in Modal Logic,Noosa,Australia,Sep 25-28,2006,6:1-26.

[7]Nalon C,Dixon C.Clausal resolution for normal modal logics[J].Journal ofAlgorithms,2007,62(3):117-134.

[8]Wu Xia,Yu Haihong,Li Zehai,et al.Relational extension rule[J].Journal of Jilin University:Science Edition,2008, 46(3):504-508.

[9]Benzmüller C,Raths T.HOL based first-order modal logic provers[C]//LNCS 8312:Proceedings of the 19th International Conference on Logic for Programming,Artificial Intelligence,and Reasoning,Stellenbosch,South Africa, Dec 14-19,2013.Berlin,Heidelberg:Springer,2013:127-136.

[10]Kaminski M,Tebbi T.InKreSAT:modal reasoning via incremental reduction to SAT[C]//LNCS 7898:Proceedings of the 24th International Conference on Automated Deduction,Lake Placid,USA,Jun 9-14,2013.Berlin,Heidelberg: Springer,2013:436-442.

[11]Rajeev G,Kerry O,Jimmy T.Implementing tableau calculi using BDDs:BDDTab system description[C]//LNCS 8562: Proceedings of the 7th International Joint Conference on Automated Reasoning,Vienna,Austria,Jul 19-22,2014.Berlin,Heidelberg:Springer,2014:337-343.

[12]Lin Hai,Sun Jigui,Zhang Yimin.Theorem proving based on the extension rule[J].Journal of Automated Reasoning, 2003,31(1):11-21.

[13]Sun Jigui,Li Ying,Zhu Xingjun,et al.A novel theorem proving algorithm based on extension rule[J].Journal of Computer Research and Development,2009,46(1):9-14.

[14]Lin Hai,Sun Jigui.Knowledge compilation using the extension rule[J].Journal of Automated Reasoning,2004,32(2): 93-102.

[15]Li Ying,Sun Jigui,Wu Xia,et al.Extension rule algorithms based on IMOM and IBOHM heuristics strategies[J].Journal of Software,2009,20(6):1521-1527.

[16]Lai Yong,Ouyang Dantong,Cai Dunbo,et al.Model counting and planning using extension rule[J].Journal of Computer Research and Development,2009,46(3):459-469.

[17]Yin Minghao,Lin Hai,Sun Jigui.Solving#SAT using extension rules[J].Journal of Software,2009,20(7):1714-1725.

[18]Yin Minghao,Sun Jigui,Lin Hai,et al.Possibilistic extension rules for reasoning and knowledge compilation[J]. Journal of Software,2010,20(11):2826-2837.

[19]Liu Lei,Niu Dangdang,Lv Shuai.Knowledge compilation methods based on the hyper extension rule[J].Chinese Journal of Computers,2016,39(8):1681-1696.

[20]Zhou Beihai.Introduction to modal logic[M].Beijing:Peking University Press,1997.

附中文參考文獻：

[8]吳瑕,于海鴻,李澤海,等.關系擴展規則[J].吉林大學學報:理學版,2008,46(3):504-508.

[13]孫吉貴,李瑩,朱興軍,等.一種新的基于擴展規則的定理證明算法[J].計算機研究與發展,2009,46(1):9-14.

[15]李瑩,孫吉貴,吳瑕,等.基于IMOM和IBOHM啟發式策略的擴展規則算法[J].軟件學報,2009,20(6):1521-1527.

[16]賴永,歐陽丹彤,蔡敦波,等.基于擴展規則的模型計數與智能規劃方法[J].計算機研究與發展,2009,46(3):459-469.

[17]殷明浩，林海，孫吉貴.一種基于擴展規則的#SAT求解系統[J].軟件學報,2009,20(7):1714-1725.

[18]殷明浩，孫吉貴，林海,等.可能性擴展規則的推理和知識編譯[J].軟件學報,2010,21(11):2826-2837.

[19]劉磊,牛當當,呂帥.基于超擴展規則的知識編譯方法[J].計算機學報,2016,39(8):1681-1696.

[20]周北海.模態邏輯導論[M].北京:北京大學出版社,1997.

YANG Yang was born in 1992.He is an M.S.candidate at Jilin University.His research interests include intelligent planning,automated reasoning and cloud computing,etc.

楊洋（1992—），男，吉林大學碩士研究生，主要研究領域為智能規劃，自動推理，云計算等。

LI Guangli was born in 1992.He is an M.S.candidate at Jilin University.His research interests include automated reasoning,cloud computing and parallel programming,etc.

李廣力（1992—），男，吉林大學碩士研究生，主要研究領域為自動推理，云計算，并行編程等。

ZHANG Tongbo was born in 1995.He is a student at Jilin University.His research interests include automated reasoning,cloud computing and parallel programming,etc.

張桐搏（1995—），男，吉林大學學生，主要研究領域為自動推理，云計算，并行編程等。

LIU Lei was born in 1960.He received the M.S.degree in computer software from Jilin University in 1985.Now he is a professor and Ph.D.supervisor at Jilin University.His research interest is software theory and technology.

劉磊（1960—），男，吉林長春人，吉林大學教授、博士生導師，主要研究領域為軟件理論與技術。累計發表學術論文180余篇，主持國家自然科學基金等科研項目30余項。

LV Shuai was born in 1981.He received the Ph.D.degree in computer software and theory from Jilin University in 2010.Now he is an associate professor at Jilin University.His research interests include intelligent planning and automated reasoning,etc.

呂帥（1981—），男，吉林公主嶺人，2010年于吉林大學獲得博士學位，現為吉林大學副教授，主要研究領域為智能規劃，自動推理等。累計發表學術論文61篇，主持國家自然科學基金等科研項目7項，獲得全國商業科技進步一等獎2項、吉林省科學技術進步三等獎2項。

Parallel Reasoning Methods in Propositional Modal Logic S5*

YANG Yang1,LI Guangli1,ZHANG Tongbo1,LIU Lei1,LV Shuai1,2,3+
1.College of Computer Science and Technology,Jilin University,Changchun 130012,China
2.College of Mathematics,Jilin University,Changchun 130012,China
3.Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University),Ministry of Education, Changchun 130012,China
+Corresponding author:E-mail:lus@jlu.edu.cn

S5 system is a special and important axiomatic system in propositional modal logic that has great ability of knowledge representation and processing,which is the basis of non-classical logics such as epistemic logic and belief logic etc.According to Kripke semantic model and part of the axioms in S5 system,this paper gives a more indepth research on the characteristics of propositional modal logic S5,and analyzes the features of a kind of representative formulae which is standard modal clauses,then proposes an NER-based algorithm called PMCRNER(propositional modal clausal reasoning based on novel extension rule)which is used to reason for standard modal clauses in propositional modal logic S5.In the view of high time complexity in simple algorithm,this paper uses the potential relevance between tasks to make the algorithm parallel in the degree of coarse-granularity and fine-granularity.This paper also gives the theoretical framework of PPMCRNER(parallel PMCRNER)and compares it with the basic algorithm.The experiments show that PPMCRNER has good speedup on unsatisfiable clause sets,and provides a feasible scheme for further research on the reasoning methods for modal formulae which are hard to solve.

propositional modal logic;S5 axiom system;parallel reasoning;extension rule

10.3778/j.issn.1673-9418.1509035

A

TP181

*The National Natural Science Foundation of China under Grant Nos.61300049,61502197,61503044(國家自然科學基金);the Specialized Research Fund for the Doctoral Program of Higher Education of China under Grant No.20120061120059(高等學校博士學科點專項科研基金).

Received 2015-09,Accepted 2015-11.

CNKI網絡優先出版:2015-12-03,http://www.cnki.net/kcms/detail/11.5602.TP.20151203.0826.002.html