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

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

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

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

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

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

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

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

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

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