描述逻辑 ALC 中的推理优化表格算法

HAL Id: tel-03885469https://theses.hal.science/tel-03885469Khadija Jradeh0提交日期：2022年12月5日0HAL是一个多学科的开放获取存档，用于存储和传播科学研究文献，无论其是否发表。这些文献可以来自法国或国外的教育和研究机构，或者来自公共或私人研究中心。0HAL多学科开放获取存档，用于存储和传播研究级科学文献，无论是否发表，来自法国或国外的教育和研究机构，公共或私人实验室。0在扩展了链接键的描述逻辑 ALC中进行推理的优化表格算法0引用此版本：0Khadija Jradeh. 在扩展了链接键的描述逻辑 ALC 中进行推理的优化表格算法. 其他 [cs.OH].格勒诺布尔阿尔卑斯大学 [2020-..], 2022. 英语. �NNT : 2022GRALM021�. �tel-03885469� 0博士学位论文0获得学位：0格勒诺布尔阿尔卑斯大学博士0博士学位授予单位：MSTII -数学、科学和信息技术，计算机科学专业：格勒诺布尔计算机实验室0在扩展了链接键的描述逻辑 ALC 中进行推理的优化表格算法0在扩展了链接键的描述逻辑 ALC 中进行推理的优化表格算法0提交者：Khadija JRADEH0博士导师：0Manuel ATENCIA ARCAS 格勒诺布尔阿尔卑斯大学0博士导师0Chan LE DUC巴黎北索邦大学0博士导师0评审人：0MADALINA CROITORU 教授，蒙彼利埃大学 NATHALIEPERNELLE 教授，巴黎北索邦大学0博士论文公开答辩日期：2022年7月12日，答辩委员会成员：0MADALINA CROITORU 教授，蒙彼利埃大学0评审人0NATHALIE PERNELLE 教授，巴黎北索邦大学0评审人0JERÔME GENSEL 教授，格勒诺布尔阿尔卑斯大学0主席0CASSIA TROJAHN DOS SANTOS高级讲师，图卢兹第二大学 - 让∙若尔斯大学0考官0受邀嘉宾：1.1.1Knowledge representation on the semantic web . . . . . . . . . . . . .101.1.3Link keys . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .121.3Contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .132Preliminaries162.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .162.2.2Reasoning problems and services. . . . . . . . . . . . . . . . . . . .182.2.3Reduction of ontology entailment to ontology consistency . . . . . . .182.2.4Extension of ALC with inverse roles I. . . . . . . . . . . . . . . . .192.3Tableau algorithms for reasoning in ALC. . . . . . . . . . . . . . . . . . . .192.4Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .203Literature Review213.1Reasoning in description logics with ontological constraints . . . . . . . . . . .213.1.1Tableau algorithms for reasoning in description logics. . . . . . . . .223.1.2Reasoning with keys . . . . . . . . . . . . . . . . . . . . . . . . . . .223.1.2.1Reasoning with keys in a separate set of constraints. . . . .223.1.2.2Reasoning with keys as a new concept constructor . . . . . .243.1.2.3Link keys cannot be reduced to keys. . . . . . . . . . . . .243.1.2.4Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . .243.1.3Reasoning with rules . . . . . . . . . . . . . . . . . . . . . . . . . . .243.1.3.1Reasoning with DL-safe rules . . . . . . . . . . . . . . . . .253.1.3.2Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . .263.1.4Reasoning with correspondences . . . . . . . . . . . . . . . . . . . . .263.1.4.1Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . .283.2The complexity of reasoning in the description logic ALC and its simple ex-tensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .283.2.1Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .303.3Summary. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3020目录01 引言 10 1.1 背景 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1001.1.2 RDF图的互联 . . . . . . . . . . . . . . . . . . . . . . . . 1101.2 问题陈述 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1201.4 组织 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1502.2 描述逻辑 ALC 及其扩展 . . . . . . . . . . . . . . . . . . 164A 2EXPTIME tableau algorithm for reasoning in the description logic ALC withlink keys and individual equalities314.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .314.2The description logic ALC+LK . . . . . . . . . . . . . . . . . . . . . . . . .324.3Reduction of ontology entailment to ontology consistency. . . . . . . . . . .334.4Tableau algorithm for ALC+LK . . . . . . . . . . . . . . . . . . . . . . . . .344.4.1Preprocessing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .344.4.2Blocking. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .344.4.3Clashes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .354.4.4Completion rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . .364.5Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .384.6Properties of the method. . . . . . . . . . . . . . . . . . . . . . . . . . . . .414.6.1Some properties of derived ontologies . . . . . . . . . . . . . . . . . .414.6.2Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .424.6.3Soundness. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .434.6.4Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .484.6.5Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .504.7Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .515A worst-case optimal EXPTIME algorithm for reasoning in the description logicALC with link keys and individual equalities525.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .525.2A compressed tableau for the description logic ALC+LK. . . . . . . . . . .535.3A non-directed algorithm for the description logic ALC+LK . . . . . . . . . .595.4Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .625.5Properties of the algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . .645.5.1Soundness. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .645.5.2Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .685.5.3Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .715.6Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .756A worst-case optimal EXPTIME tableau algorithm for reasoning in the descriptionlogic ALC extended with link keys and individual equalities766.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .766.2A Compressed Tableau for the logic ALC+LK . . . . . . . . . . . . . . . . .766.3Compressed Tableau Algorithm. . . . . . . . . . . . . . . . . . . . . . . . .786.4Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .976.5Properties of the algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . .996.5.1Soundness. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .996.5.2Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1026.5.3Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1076.6Extending ALC+LK with inverse roles . . . . . . . . . . . . . . . . . . . . . 1086.7Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10937Implementation and Evaluations1107.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1107.2Star´eLK architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1107.2.1Datasets, ontologies, and alignments parser module . . . . . . . . . . . 1117.2.2Link keys parser module . . . . . . . . . . . . . . . . . . . . . . . . . 1117.3Evaluations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1137.3.1Correctness of Star´eLK . . . . . . . . . . . . . . . . . . . . . . . . . . 1137.3.1.1Experimental goals. . . . . . . . . . . . . . . . . . . . . . 1137.3.2Impact of link key reasoning on data interlinking . . . . . . . . . . . . 1147.3.2.1Experimental goals. . . . . . . . . . . . . . . . . . . . . . 1157.4Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1188.2Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120Bibliography128407.2.3 推理模块 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11207.3.1.2 实验设置和结果 . . . . . . . . . . . . . . . . 11307.3.2.2 实验设置和结果 . . . . . . . . . . . . . . . . 11608 结论与展望 119 8.1 总结与结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11909 附录 122 9.1 扩展描述逻辑  ALC 与逆角色 . . . . . . . . . . . . . 1221Tableau algorithm for ALC+LK ontology consistency checking . . . . . . . . .363Compressed algorithm for ALCLK ontology consistency checking. . . . . .614init algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .825matchCore algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .836matchTriple algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .867matchMerge algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .898check algorithm. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .939Compressed tableau algorithm for ALC+LK ontology consistency checking . . . . . .9750算法列表02 压缩表格剪枝算法 . . . . . . . . . . . . . . . . . . . . 61List of Figures2.1Completion rules for ALC. . . . . . . . . . . . . . . . . . . . . . . . . . . . .204.1Completion rules for ALC+LK. . . . . . . . . . . . . . . . . . . . . . . . . .374.2Derived ABox corresponding to A6 in Example 6. . . . . . . . . . . . . . . . .444.3Left: Canonical interpretation corresponding to the derived ABox of Figure 4.2.455.1Graphical representation of the triple τ.. . . . . . . . . . . . . . . . . . . . .545.2A star-type made up of 3 triples. . . . . . . . . . . . . . . . . . . . . . . . . .545.4An invalid and a valid star-type built from O.. . . . . . . . . . . . . . . . . .565.5The star-types σa and σb satisfy the condition of λ through the star-types σdand σe.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .585.6A pair of ABoxes generated upon the application of non-deterministic rule inthe standard tableau algorithms.. . . . . . . . . . . . . . . . . . . . . . . . .595.7A pair of star-types generated upon the application of non-deterministic rule inthe compressed tableau algorithm. . . . . . . . . . . . . . . . . . . . . . . . .605.8Valid star-types that do not satisfy ({⟨P, Q⟩} linkkey ⟨C, D⟩). . . . . . . . . . .635.9A compressed tableau CT = ⟨⟨Λ0, Λ1, Λ2⟩, Ω⟩ for O. . . . . . . . . . . . . . .646.1The figure on the right hand side is not saturated star-type while figure on theleft hand side is saturated. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .776.2Completion rules applied on a star-type σ. . . . . . . . . . . . . . . . . . . . .796.3Link key and equality rules applied to star-types in Λ0.. . . . . . . . . . . . .806.4Application of matchCore algorithm . . . . . . . . . . . . . . . . . . . . . . .836.5When there is a triple is ρ′ ∈ σ′ and ρ′ ̸∈ σ the algorithm creates a ρ′-successorof σ′ and adds it to Λ.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .876.6A part of the pre-compressed tableau before and after applying Algorithm 6. . .876.7matchMerge transforms the predecessors of star-types σ ⊕ σ′={τ1, τ2} . . . . .907.1Star´eLK architecture. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1117.2The components of Star´eLK reasoning module. . . . . . . . . . . . . . . . . . 1127.3Data interlinking pipeline based on link key inference.. . . . . . . . . . . . . 1159.1Matching function between star-types, (ω, ρ) ∈ Ω(σ, τ).. . . . . . . . . . . . 1236AcknowledgementI like first to thank the reviewers, Mme Madalina Croitoru and Mme Nathalie Pernelle fortheir valuable reviews and comments. I would like to thank Mme Madalina Croitoru, also, forthe support and the encouragement she gave me during the thesis follow-up meetings. I wantto thank Mme Cassia Trojahn Dos Santos for being on the jury and for providing me the op-portunity to do my post-doctoral research with her. Also, I am very thankful to the president ofthe jury M. Jérôme Gensel for all the interesting discussions.70我还要衷心感谢我的论文导师Manuel AtenciaArcas，感谢他在我的论文中给予我的鼓励和建议，无论是在科学上还是在个人上。能与您一起工作是一次很好的机会。我还要感谢我的共同导师Chan LeDuc，感谢他传授给我的大量知识，并始终坚持让我展现最好的自己。0我真诚地感谢mOeX团队成员们的支持和鼓励。特别感谢JérômeEuzenat给予我的指导、反馈和评论，这些帮助我塑造和改进我的研究。同时，我还要感谢JérômeDavid在科学和个人方面提供的所有帮助。我还要感谢mOeX的同事和朋友Yasser和Andreas，他们让我的旅程更加丰富和愉快。0我对我的家人，特别是我的母亲Samira和父亲Mahmoud深表感激，感谢他们持续的关心和爱。无论我们之间有多远的距离，感谢你们一直在我身边。没有你们，我永远无法完成这一切。0对于我的朋友Mayssam、Samarmar和Zainab，感谢你们成为我的第二个家庭。我永远不会找到像你们这样支持和关心我的朋友。0对于我的伴侣Shadi，感谢你一直在我身边。感谢你的耐心、支持和爱，给了我追求博士学位的力量。80简历0知识图谱（KG）被不同的组织不断地用来以图形的形式表示现实世界中的实体。它们可以使用本体层来描述所表示实体的类和属性。RDF知识图谱是将知识图谱传输到RDF模型的知识图谱。RDF知识图谱的互联是指识别属于不同RDF知识图谱的不同IRI，并引用同一现实世界实体。这通过将不同知识图谱中存在的实体的不同描述组合起来，从而促进数据的集成和互操作性。有多种方法可以处理RDF知识图谱的互联任务，链接键是其中之一。它们用于连接使用不同本体描述的RDF知识图谱。链接键指定要比较的属性，以确定不同类别中的两个实体是否相同。链接键可以用逻辑公理的形式表示，因此可以与本体和本体对齐相结合进行逻辑推理。在本论文中，我们的目标是研究使用链接键进行推理的问题。为了形式化研究这个问题，我们使用描述逻辑ALC对RDF知识图谱、本体和本体对齐进行建模。我们选择描述逻辑ALC作为推理的基本语言。ALC涵盖了许多用于知识表示的建模能力，并且可以更容易地扩展到更具表达力的描述逻辑。我们使用链接键和个体相等性扩展ALC，得到的描述逻辑称为ALC +LK。我们证明了链接键的蕴含可以简化为验证链接键的一致性，而不需要引入链接键的否定。然后，我们设计了一个算法来判断ALC +LK本体的一致性。我们证明了该算法的正确性、完备性和终止性。该算法的时间复杂度为2E XPT IME。然而，对于ALC的推理存在E XP TIME算法，并且为了处理链接键和个体相等性而添加的补全规则不需要比ALC更高的计算能力。基于上述情况，我们设计了一个在最坏情况下具有正确性、完备性和最优性的ALC +LK推理算法。该算法受到压缩表算法的启发，可以获得最优的复杂性结果E XP TIME。然而，该算法具有非定向性的行为，这阻碍了它的实现。最后但并非最不重要的是，我们提出了一个在最坏情况下具有正确性、完备性和最优性的表格推理算法，用于描述逻辑ALC中的个体和链接键的推理。与非定向算法不同，该算法通过应用补全规则来进行定向。这避免了生成无用结构并简化了其实现。我们实现了该算法，并提供了一些概念证明实验，证明了链接键对数据互联任务的重要性。90摘要0知识图（KG）被不同的组织不断地用来以图形的形式表示现实世界的实体。它们可以使用本体层来描述所表示实体的类和属性。RDF知识图是传达给RDF模型的知识图。RDF知识图互连是识别属于不同RDF知识图并指向同一现实世界实体的不同IRI的任务。这通过组合不同知识图中存在的不同实体描述来促进数据集成和互操作性。存在不同的方法来解决RDF知识图互连任务。链接键是其中之一。它们用于链接使用不同本体描述的RDF知识图。链接键指定要比较的属性，以决定属于不同类并存在于不同知识图中的两个实体是否相同。链接键可以表示为逻辑公理，因此可以将它们与本体和本体对齐组合起来进行逻辑推理。在本论文中，我们旨在研究使用链接键进行推理的问题。为了正式研究这个问题，我们使用描述逻辑ALC对RDF知识图、本体和本体对齐进行建模。我们选择描述逻辑ALC作为推理的基本语言。ALC涵盖了许多用于知识表示的建模能力，并允许更容易地扩展到更具表现力的描述逻辑。我们使用链接键和个体相等性扩展ALC，得到的描述逻辑称为ALC +LK。我们证明了链接键蕴含可以简化为链接键一致性检查，而不需要引入链接键的否定。然后我们设计了一个用于判断ALC +LK本体一致性的算法。我们证明了该算法是完备、正确且总是终止的。该算法运行时间为2EXP T IME。然而，对于在ALC中进行推理存在E XP TIME算法，并且为了处理链接键和相等性而添加的完成规则不需要比ALC更多的计算能力。基于上述情况，我们设计了一个在ALC +LK中进行推理的完备、最坏情况下最优的算法。该算法受到压缩表格算法的启发，可以获得EXP TIME最优的复杂性结果。然而，该算法具有非定向行为，这阻碍了它的实现。最后但最重要的是，我们提出了一种在描述逻辑ALC中进行推理的完备、最坏情况下最优的表格算法，该算法通过应用完成规则进行定向。这避免了生成无用结构并简化了其实现。我们实现了该算法，并提供了一些概念验证实验，证明了使用链接键进行数据互连任务的重要性。100第1章0引言0“...当你将数据连接在一起时，你就会获得力量。”蒂姆∙伯纳斯-李0在本章中，我们在第1.1节中定义了RDF图的相互链接问题和链接键。我们在第1.2节中介绍了使用链接键进行推理的问题。我们在第1.3节中介绍了论文的贡献。最后，我们在第1.4节中概述了论文的大纲。01.1 上下文0语义网（SW）是通过由万维网联盟（W3C）制定的标准对万维网（WWW）进行扩展。资源描述框架（RDF）是一种W3C标准的数据表示模型。RDF模式（RDFS）和本体网语言（OWL）是用于表示有关此数据的知识的W3C标准语言。这些知识为数据添加了含义，并允许轻松交换和组合属于不同平台的数据。01.1.1 语义Web上的知识表示0知识图（KG）是以实体和它们之间的关系形式表示的结构化数据的表示。这些数据以机器可读、“理解”和提取事实的方式表示。RDF图是符合RDF模型的知识图。在RDF中，数据以三元组的形式表示。三元组由主语、谓词和宾语组成。主语和谓词是资源，而宾语可以是资源或文字。资源由国际化资源标识符（IRI）标识。RDF图通常使用本体描述。这些本体允许流畅地表示各种类型的数据描述：数据模式、分类法和词汇。这些词汇通常由一组概念（或类）和一组关系（或属性、角色）组成，表示知识领域中对象的类型和概念之间的关系。它们使用语义Web堆栈中的标准来表示：RDFS和OWL。此外，OWL具有基于描述逻辑（DL）的显式形式语义。1101.1.2 链接RDF图0RDF图通常是独立创建的。因此，它们可能包含不同的IRI，这些IRI指向同一个现实世界的实体，但没有通过owl:sameAs属性明确相关联。owl:sameAs属性将指向同一个现实世界实体的两个不同IRI链接起来。链接这些IRI可以使RDF图互补。将不同图之间的不同实体链接起来的问题称为数据链接。已经有不同的方法来解决数据链接问题。这些方法分为两大类：数值和逻辑。数值方法将数据链接的任务简化为相似性计算任务。而逻辑方法定义了一组规则或公理，规定了什么使两个实体相等。它们可以在给定的领域内重复使用，并可用于从逻辑推理中获益。数值方法通过相似性函数计算给定一对RDF图的两个不同实体之间的相似性。两个实体之间的相似性是根据给定实体对的属性值的相似性函数计算的。足够相似的实体被认为是相同的，并通过owl:sameAs属性进行链接。一些数值方法（如Silk[1]）使用户能够指定实体必须满足的条件才能进行链接。其他方法（如Limes[2]）则是完全自动的。逻辑方法又分为基于规则和基于键的方法。基于规则的方法使用规则从输入的RDF图和它们的本体中推导出标识链接[3, 4,5]。基于键的方法旨在提取一组键。每个键由一组属性和一个类组成，这些属性允许唯一标识属于指定类的实例。根据这个定义，具有键属性的相同值的两个实例被认为是相同的。更准确地说，键的形式如下：0({p1，...，pk}键C)0其中p1，...，pk是属性，C是一个类。一个键的示例如下：0({creator，title}键Work)（1.1）0声明，每