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