描述邏輯

由於描述邏輯在很多不同應用領域中都有較好的應用，這使得描述邏輯的結果變得越來越重要。實際上描述邏輯在許多領域中被作為知識表示的工具，如信息系統（Catarci,1993）,數據庫（Borgida,1995;Bergamaschi1992;Sheth,1993）軟件工程(Devambu,1991)，網絡智能訪問（Levy，1996；Blanco，1994）和規劃（Seida,1992）。上述的許多文章中都指出，對許多相應的應用領域通常需要DL的整體能力。（Doyle1991）

描述邏輯最開始只是用來表示靜態知識的。為了考慮在時間上的變化，或者在一定動作下的變化，以及保持其語言的相對簡單性，很自然地我們需要通過相應的模態算子來擴展它，以保留其命題模態狀態。眾所周知，即使只是對簡單的模態系統的綜合，也可能會導致很複雜的系統。Schild，Schmiedel等人最初所構造的時序描述邏輯和認知邏輯要麼就是因為表達能力太強而導致不可判定性，要麼就是太弱（時態算子僅僅對公式或者概念是可用的）。Baader和Laux[2]則進行了折中，將描述邏輯ALC與多態K相結合，允許將模態算子使用到公式和概念上，並證明在擴展領域模型中的結果語言的滿足性問題是可判定的。Wolter等對具有模態算子的描述邏輯進行了深入系統的調查分析，並證明在恆定的領域假設下多種認知和時序描述邏輯是可判定的。他將將描述邏輯和命題動態邏輯PDL相結合，提出了動態描述邏輯。

為了對動作和規劃能在統一的框架下進行表示和推理，A.Artale和E.Franconi(1998)提出了一個知識表示系統，用時間約束的方法將狀態、動作和規劃的表示統一起來。為了能使該表示方法進行有效的推理和具有明確的語義，它又和描述邏輯結合起來，從而形成了一個很好的知識表示方法。它具有以下優點：(i)能用統一的方法表示狀態、動作和規劃，這一點與情景演算不同；(ii)能進行高效的推理，該框架下的可滿足性問題和包含檢測問題等都是多項式時間；(iii)有明確的語義；(iv)能自動進行規劃識別。

可滿足性問題是描述邏輯推理中的核心問題，因為其它許多問題（如包含檢測、一致性問題等）都可化為可滿足性問題。為了能用計算機自動判斷描述邏輯中可滿足性問題，Schmidt-Schaub和Smolka首先建立了基於描述邏輯ALC的Tableau算法，該算法能在多項式時間內判斷描述邏輯ALC概念的可滿足性問題。Tableau算法已用於各種描述邏輯中（如ALCN、ALCQ等），並且Tableau算法也可用於判斷實例檢測等問題。主要研究各種描述邏輯中Tableau算法的擴展、複雜性及優化策略等。

為了能讓描述邏輯處理模態詞，F.Baader將模態操作引入描述邏輯。證明了該描述邏輯公式的可滿足性問題是可判定的。結合可能世界語義和可達關係，引入時間依賴和信念等模態操作，提出了多維描述邏輯框架，該描述邏輯較好的刻畫了多主體系統模型。主要研究工作集中在建立合理的模態公理及多維描述邏輯。在描述邏輯中第一個整合時間的方法是由A.Schmiedel提出來的。他使用了兩個時間運算符來擴展描述邏輯，提出了在時間段上受限的全稱和存在量詞。Schild提出了一種簡單的時序擴張，利用時態邏輯(tenselogic)中在時間點“自從”Since和“直到”Until上的時序運算符來討論ALC邏輯。