Complexity of Description Logics with Concrete Domains [PhD Thesis]

1 Introduction 1
2 Preliminaries 9
2.1 Description Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.1.1 Introducing ALC . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.1.2 Extensions of ALC . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.2 TBox and ABox Formalisms . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2.1 TBoxes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.2.2 ABoxes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.3 Description Logics with Concrete Domains . . . . . . . . . . . . . . . . 24
2.3.1 Introducing ALC(D) . . . . . . . . . . . . . . . . . . . . . . . . 24
2.3.2 Extensions of ALC(D) . . . . . . . . . . . . . . . . . . . . . . . 28
2.4 Examples of Concrete Domains . . . . . . . . . . . . . . . . . . . . . . 31
2.4.1 Unary Concrete Domains and ALCf(D) . . . . . . . . . . . . . 31
2.4.2 Expressive Concrete Domains . . . . . . . . . . . . . . . . . . . 36
2.4.3 Temporal Concrete Domains . . . . . . . . . . . . . . . . . . . 36
3 Reasoning with ALCF(D) 41
3.1 Concept Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.1.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.1.2 The Completion Algorithm . . . . . . . . . . . . . . . . . . . . 44
3.1.3 Correctness and Complexity . . . . . . . . . . . . . . . . . . . . 49
3.2 ABox Consistency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
3.2.1 The Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
3.2.2 Correctness and Complexity . . . . . . . . . . . . . . . . . . . . 62
3.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
4 Acyclic TBoxes and Complexity 67
4.1 PSpace Upper Bounds . . . . . . . . . . . . . . . . . . . . . . . . . . 68
4.1.1 ALC with Acyclic TBoxes . . . . . . . . . . . . . . . . . . . . . 68
4.1.2 A Rule of Thumb . . . . . . . . . . . . . . . . . . . . . . . . . . 74
4.1.3 ALC-ABox Consistency . . . . . . . . . . . . . . . . . . . . . . 76
4.2 A Counterexample: ALCF . . . . . . . . . . . . . . . . . . . . . . . . 78
4.3 The Upper Bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
4.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
5 Extensions of ALC(D) 95
5.1 A NExpTime-complete Variant of the PCP . . . . . . . . . . . . . . . 96
5.2 A Concrete Domain for Encoding the PCP . . . . . . . . . . . . . . . 102
5.3 Lower Bounds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
5.3.1 ALC(D)-concept Satisfiability w.r.t. Acyclic TBoxes . . . . . . 110
5.3.2 ALCu(D)-concept Satisability . . . . . . . . . . . . . . . . . . 113
5.3.3 ALC(D)-concept Satisfiability . . . . . . . . . . . . . . . . . . 115
5.3.4 ALCP(D)-concept Satisfiability . . . . . . . . . . . . . . . . . . 120
5.3.5 ALCrp(D)-concept Satisfiability . . . . . . . . . . . . . . . . . . 123
5.4 The Upper Bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128
5.4.1 The Completion Algorithm . . . . . . . . . . . . . . . . . . . . 130
5.4.2 Termination, Soundness, and Completeness . . . . . . . . . . . 134
5.4.3 Adding Acyclic TBoxes . . . . . . . . . . . . . . . . . . . . . . 149
5.5 Comparison with ALCF . . . . . . . . . . . . . . . . . . . . . . . . . . 154
5.5.1 ALCFu-concept Satisfiability . . . . . . . . . . . . . . . . . . . 154
5.5.2 Undecidability of ALCF . . . . . . . . . . . . . . . . . . . . . 156
5.6 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158
6 Concrete Domains and General TBoxes 161
6.1 An Undecidability Result . . . . . . . . . . . . . . . . . . . . . . . . . 162
6.2 ALC(P) with General TBoxes . . . . . . . . . . . . . . . . . . . . . . . 163
6.2.1 Temporal Reasoning with ALC(P) . . . . . . . . . . . . . . . . 164
6.2.2 A Modelling Example . . . . . . . . . . . . . . . . . . . . . . . 165
6.2.3 Deciding Concept Satisfiability . . . . . . . . . . . . . . . . . . 168
6.2.4 Deciding ABox Consistency . . . . . . . . . . . . . . . . . . . . 184
6.3 Related Work and Discussion . . . . . . . . . . . . . . . . . . . . . . . 194
7 Summary and Outlook 197
Bibliography 201
Index 214