檢查OWL表達式之間的邏輯蘊涵關係？

Question

我有一個簡單的問題，我懷疑沒有簡單的答案。從本質上講，我想檢查一個OWL表達式（#B）在邏輯上是否跟隨另一個（#A） - 是否是真的 - 換句話說，我想問：真的，#A - > #B？

這樣做的原因是，我正在寫一個匹配算法相匹配在基於知識（由#KnowledgeStructure類表示）的結構的應用程序來描述當前應用狀態的需要的結構（#StateRequirement ）。這兩個結構都具有屬性，它們具有代表第三種結構（#Model）狀態下的OWL表達式的字符串值。它們是：＃KnowledgeStructure.PostCondition，它表示如何將應用於#Model的知識結構轉換#Model;和＃StateRequirement.GoalCondition，它表達了應用程序想實現的#Model狀態。因此，我希望看到#KnowledgeStructure是否會通過檢查＃KnowledgeStructure.PostCondition生成所需的＃StateRequiremment.GoalCondition來滿足#StateRequirement。我可以抽象表達爲：（＃KnowledgeStructure.Postcondition =>＃StateRequirement.GoalCondition）=>匹配（#KnowledgeStructure，#StateRequirement）。不太容易混淆，我可以表示爲：（（#A - > #B） - >匹配（#A，#B）），其中#A和#B都是有效的OWL表達式。

在一般情況下，我希望能夠表達以下規則：「如果#A表達式#A跟隨來自#A，那麼表達式匹配（#A，#B）也是真的」 。

本質上，我的問題是這樣的：我如何在OWL中構建或實現這樣的規則？我如何測試一個表達式是否來自另一個表達式？另外，如果這個關係沒有明確說明，現有的reasoners是否足夠強大以確定兩個表達式之間的關係#A - > #B？

Answer 1

我不是100％確定我完全理解了這個問題，但是從我所掌握的情況來看，我會以這種方式來面對這種情況。

首先，我指的是Java，因爲我知道的所有庫都是針對這種語言的。其次，我不認爲OWL本身能夠滿足你的目標，因爲它可以代表規則和公理，但它不提供推理，也就是說，你需要一個推理者，所以你需要建立一個程序使用它，再加上做我會在下面草繪的額外處理：

1）你沒有提到它，但我想你有一個基礎的本體wrt你需要證明你的後果關係（你用符號「 - >」表示）。如果本體不明確，也許它可以從你在問題中提到的文本表達中提取/組成。

2）您需要使用庫進行本體操作，我建議來自曼徹斯特大學的OWL API，它非常強大且簡單，在教程的「文檔」一節中您可以看到主要功能的概述，包括使用reasoners（這個例子顯示了隱士，但這個原則適用於其他任何推理者）。

3）此時，您需要檢查，如果本體是一致的（否則什麼都可以得到，因爲它往往以虛假的前提發生）

4）你下面的公理添加到本體（你打造它直接在Java中，不需要序列化回來，你可以讓推理器在內存表示上工作）並檢查一致性：A \ sqsubseteq B，即使用相關的解釋：A^I \ subseteq B^I ，所以它相當於A => B（它們具有相同的真值表）。

5）此時，您可以添加公理Match（A，B），其中A和B是您的類表達式，而Match是一個角色/關係，它涉及所有類表達式，其中第二個是首先。

6）經過多次重複這些步驟之後，您可能需要對結果進行序列化並將其存儲起來，這可以通過使用OWL API從內存表示中很簡單地實現。

有關描述邏輯（OWL本體的基礎邏輯）的一些基礎知識，可以參考A description logic Primer (2012), Horrocks et al.和Foundations of Description Logics (2011), Rudolph。

我不是一個邏輯學家或DL專家，所以請覈實我所提供的信息，並隨時糾正我:)