دانلود کتاب Tableau-based Reasoning for Description Logics with Inverse Roles and Number Restrictions [PhD Thesis]

فهرست مطالب :

Abstract iii List of Tables ix List of Figures x 1 Introduction 1 1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Tbox, Abox and Role Hierarchy . . . . . . . . . . . . . . . . . . . . . 7 1.3.1 Tbox . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.3.2 Abox . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.3.3 Role Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.5 Research Motivation, Contribution and Report Organization . . . . . 14 1.5.1 Research Motivation . . . . . . . . . . . . . . . . . . . . . . . 14 1.5.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 1.5.3 Report Organization . . . . . . . . . . . . . . . . . . . . . . . 17 2 Dynamic Tableaux Caching for ALCI 20 2.1 The Tableaux Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.2 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 InverseRole and ALCI Abox 31 3.1 An Equivalence on Inverse Relation . . . . . . . . . . . . . . . . . . . 31 3.2 Abox Consistency with Acyclic Tbox . . . . . . . . . . . . . . . . . . 33 3.2.1 The Intuition Behind the Conversion . . . . . . . . . . . . . . 33 3.2.2 The Three Steps . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.2.3 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 4 A Tableaux Procedure for ALCFI 46 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 4.1.1 A Brief Review . . . . . . . . . . . . . . . . . . . . . . . . . . 46 4.1.2 Why Inverse Relation Is The Problem. . . . . . . . . . . . . . 48 4.1.3 A New Approach . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.2 ALCFI Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . 53 4.3 A Preprocessing Step . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 4.4 ALCFI Tableau Rules . . . . . . . . . . . . . . . . . . . . . . . . . . 56 4.5 ALCFI Decision Procedure . . . . . . . . . . . . . . . . . . . . . . . 59 4.5.1 The Procedure TEST(.,.) . . . . . . . . . . . . . . . . . . . . 59 4.5.2 The Procedure SAT(.,.,.,.) . . . . . . . . . . . . . . . . . . 61 4.5.3 The Sub-Procedure Successors(.,.,.) . . . . . . . . . . . . 62 4.5.4 The Sub-Procedure AllSuccessors(.,.) . . . . . . . . . . . 63 4.6 Equisatisfiability of the Preprocessing Step . . . . . . . . . . . . . . . 63 4.7 Correctness of the Decision Procedure . . . . . . . . . . . . . . . . . . 67 4.7.1 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 4.7.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 4.7.3 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 4.8 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 5 SHOI, SHQ, and ALCHQI Acyclic Tbox 78 5.1 Reducing SHQ to ALCQ . . . . . . . . . . . . . . . . . . . . . . . . 78 5.2 Reducing SHOI to SHO . . . . . . . . . . . . . . . . . . . . . . . . 80 5.3 Reducing ALCHQI Acyclic Tbox . . . . . . . . . . . . . . . . . . . . 82 5.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 6 A Tableaux Procedure for SHIQ 88 6.1 Two Questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 6.1.1 Big Number Values . . . . . . . . . . . . . . . . . . . . . . . . 88 6.1.2 Soundness of Tableaux Caching . . . . . . . . . . . . . . . . . 89 6.2 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 90 6.3 The Algebraic Method for SHIQ . . . . . . . . . . . . . . . . . . . . 93 6.3.1 Fine-tuning onModal Constraints . . . . . . . . . . . . . . . . 94 6.3.2 Atomic Decomposition and Integer Linear Program . . . . . . 95 6.3.3 A Concatenated Two-phase Decomposition . . . . . . . . . . . 98 6.3.4 Tableaux Structure . . . . . . . . . . . . . . . . . . . . . . . . 99 6.4 SHIQ Tableaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 6.4.1 Tableau Expansion Rules . . . . . . . . . . . . . . . . . . . . . 100 6.4.2 Inconsistency Propagation Rules . . . . . . . . . . . . . . . . . 101 6.4.3 Blocking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 6.5 SHIQ Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 6.6 Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 6.6.1 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 6.6.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 6.6.3 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 6.7 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 6.7.1 Integer Linear Inequation . . . . . . . . . . . . . . . . . . . . 114 6.7.2 Atomic Decomposition . . . . . . . . . . . . . . . . . . . . . . 114 6.7.3 Reachability Analysis . . . . . . . . . . . . . . . . . . . . . . . 115 6.8 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 6.9 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 7 Conclusion and Future Work 121 7.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 7.2 Conclusion and Future Research Direction . . . . . . . . . . . . . . . 125 Bibliography 127 A Tableau-based Decision Procedures and Optimizations 139 A.1 Tableau-based Decision Procedures . . . . . . . . . . . . . . . . . . . 139 A.2 General Optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . 142 A.2.1 Concept Unfolding . . . . . . . . . . . . . . . . . . . . . . . . 143 A.2.2 Normalization and Simplification . . . . . . . . . . . . . . . . 145 A.2.3 Internalization . . . . . . . . . . . . . . . . . . . . . . . . . . . 146 A.2.4 Branching . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 A.2.5 Backtracking . . . . . . . . . . . . . . . . . . . . . . . . . . . 148 A.2.6 AxiomTransformation . . . . . . . . . . . . . . . . . . . . . . 149 A.2.7 Blocking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150 A.2.8 Caching Technique . . . . . . . . . . . . . . . . . . . . . . . . 151 A.3 Reasoning About Inverse Roles . . . . . . . . . . . . . . . . . . . . . 154 A.4 Reasoning About Number Restrictions . . . . . . . . . . . . . . . . . 156 B Empirical Results 158