描述邏輯及其應(yīng)用.pdf

1、主要研究面向語義Web和數(shù)據(jù)模型的描述邏輯的語義及推理，以及描述邏輯循環(huán)術(shù)語集的語義及推理。 主要工作和創(chuàng)新點包括以下幾個方面： (1)分析了描述邏輯SHOIQ(D)與語義Web的關(guān)系，特別是SHOIQ(D)與語義Web本體語言的等價性。但由于SHOIQ(D)的復(fù)雜性，目前只給出了它的語法和語義，還沒有研究給出它的推理機制。本文在描述邏輯SHOIQ推理機制的基礎(chǔ)上，提出了SHOIQ(D)的tableaux的概念，研究了基

2、于tableaux的SHOIO(D)的推理機制，提出了SHOIQ(D)-tableaux推理算法，并證明了該算法的正確性。 (2)分析了語義Web語義表示理論的研究現(xiàn)狀及存在的問題，提出了一種新的面向語義Web語義表示的模糊描述邏輯FSt-IOIQ。給出了FSHOIQ的語法和語義，提出了FSHOIQ的模糊Tableaux的概念，給出了一種基于模糊Tableaux的FSHOIQ的ABox約束下的可滿足性推理算法，證明了可滿足性推理

3、算法的正確性。提出了FSHOIQ的TBox擴展和去除方法，并證明了FSHOIQ的TBox約束下的包含推理問題可以轉(zhuǎn)化為．ABox約束下的可滿足性推理問題。FSHOIQ為語義Web表示和推理模糊知識提供了理論基礎(chǔ)。 (3)分析了目前描述邏輯的研究現(xiàn)狀和存在的問題，特別是動態(tài)描述邏輯(DDL)作為語義Web邏輯基礎(chǔ)所存在的問題。針對語義Web的特點和需求，對DDL進行了擴充，提出了一種新的描述邏輯，即分布式動態(tài)描述邏輯(D3L),給

4、出了D3L的語法和語義，并研究了D3L的推理機制，提出了兩種推理方法：直接推理和轉(zhuǎn)化推理。與動態(tài)描述邏輯DDL相比，該D3L可以為語義Web提供更為合理的邏輯基礎(chǔ)，彌補了DDL作為語義Web邏輯基礎(chǔ)的不足。 (4)分析了描述邏輯ALNUI與ER模型的關(guān)系，特別是如何將ER模型轉(zhuǎn)化為ALNUI的知識庫，從而利用ALNUI的推理機制對ER模型進行自動推理的有效性，在此基礎(chǔ)上進一步研究了基于描述邏輯的模糊ER模型。針對模糊ER模型的特

5、點和需求，在描述邏輯ALNUI的基礎(chǔ)上，對描述邏輯ALNUI進行了模糊化推廣，提出了一種新的描述邏輯，即模糊描述邏輯FALNUI。研究了基于FALNUI的模糊ER模型，即研究了如何將模糊ER模型轉(zhuǎn)化為FALNUI的知識庫，并利用FALNUI的推理機制研究了模糊ER模型的可滿足性、冗余性和包含關(guān)系等自動推理問題，證明了這些推理問題的正確性。提出了一種基于描述邏輯tableaux的FALNUI的可滿足性推理算法，證明了該推理算法的正確性。以

6、及提出了FALNUT的Tbox擴展和去除方法，證明了FALNUI的包含推理問題可以轉(zhuǎn)化為可滿足性推理問題，并給出了FALNUI的包含推理算法。FALNUI的tableaux推理算法為模糊ER模型的可滿足性、冗余性和包含關(guān)系等自動推理的實現(xiàn)提供了理論基礎(chǔ)。 (5)分析了描述邏輯在數(shù)據(jù)庫中的研究現(xiàn)狀和存在的問題，特別是描述邏輯與時序ER模型的關(guān)系，在A Artale的基礎(chǔ)上提出了一種形式化的帶屬性依賴時序ER模型εR<,VTAD>。

7、并針對帶屬性依賴時序ER模型εR<,VTAD>的需求和特點，提出了一種新的描述邏輯，即時序描述邏輯ALCQI(D)<,US>，給出了ALCQI(D)<,US>的語法和語義，研究了基于ALCQI(D)<,US>的帶屬性依賴時序ER模型，即研究了如何將帶屬性依賴時序ER模型εR<,VTAD>轉(zhuǎn)化為ALCQI(D)<,US>的知識庫，從而利用ALCQI(D)<,US>的推理機制對帶屬性依賴時序ER模型的可滿足性、冗余性、包含關(guān)系和蘊含關(guān)系等問

8、題進行自動推理，并證明了這些推理問題的正確性。 (6)分析了描述邏輯循環(huán)術(shù)語集的研究現(xiàn)狀和存在的問題，在F Baader的基礎(chǔ)上進一步研究了描述邏輯εL混合循環(huán)術(shù)語集的LCS和MSC推理問題。給出了εL混合循環(huán)術(shù)語集的語法和語義。針對εL混合循環(huán)術(shù)語集LCS和MSC推理的需要，提出了Tbox-完全的概念，并重新定義了描述圖，使用描述圖和Tbox-完全給出了最大不動點語義下εL混合循環(huán)術(shù)語集LCS和MSC的推理算法，證明了推理算法

9、的正確性，并證明了推理算法是多項式時間復(fù)雜的。 (7)分析了描述邏輯循環(huán)術(shù)語集的研究現(xiàn)狀和存在的問題，基于混合分級μ-演算將不動點構(gòu)造算子引入到含有枚舉構(gòu)造算子的描述邏輯ALCQO中，提出了一種允許包含循環(huán)術(shù)語集的描述邏輯μALCQO，給出了μALCQO的語法、語義和不動點構(gòu)造算子的性質(zhì)，證明了μALCQO的可滿足性推理等價于混合分級μ-演算的可滿足性推理，并利用完全強化自動機理論給出了μALCQO的可滿足性推理算法，以及給出了