Complexity Results and Practical Algorithms for Logics in Knowledge Representation [PhD Thesis]

1 Introduction 1
1.1 Description Logic Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Reasoning in Description Logics . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3 Expressive Description Logics . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3.1 Counting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.3.2 Transitive Roles, Role Hierarchies, and Inverse Roles . . . . . . . . 4
1.3.3 Nominals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.4 Guarded Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.5 Outline and Structure of this Thesis . . . . . . . . . . . . . . . . . . . . . . 7
2 Preliminaries 11
2.1 The Basic DL ALC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Terminological and Assertional Formalism . . . . . . . . . . . . . . . . . . 13
2.3 Inference Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
3 Reasoning in Description Logics 17
3.1 Reasoning Paradigms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.2 Tableau Reasoning for ALC-satisability . . . . . . . . . . . . . . . . . . . 20
3.2.1 Deciding Concept Satisability for ALC . . . . . . . . . . . . . . . . 21
3.2.2 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.2.3 Other Inference Problems for ALC . . . . . . . . . . . . . . . . . . . 31
4 Qualifying Number Restrictions 35
4.1 Syntax and Semantics of ALCQ . . . . . . . . . . . . . . . . . . . . . . . . 36
4.2 Counting Pitfalls . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2.1 An Incorrect Solution . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2.2 A Correct but Inecient Solution . . . . . . . . . . . . . . . . . . . 40
4.3 An Optimal Solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.3.1 Correctness of the Optimized Algorithm . . . . . . . . . . . . . . . 42
4.3.2 Complexity of the Optimal Algorithm . . . . . . . . . . . . . . . . . 47
4.4 Extensions of ALCQ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.4.1 Reasoning for ALCQIb . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.4.2 Correctness of the Algorithm . . . . . . . . . . . . . . . . . . . . . 54
4.4.3 Complexity of the Algorithm . . . . . . . . . . . . . . . . . . . . . . 59
4.5 Reasoning with ALCQIb-Knowledge Bases . . . . . . . . . . . . . . . . . . . 61
5 Cardinality Restrictions and Nominals 75
5.1 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
5.2 The Complexity of Cardinality Restrictions and Nominals . . . . . . . . . 78
5.2.1 Cardinality Restrictions and ALCQI . . . . . . . . . . . . . . . . . . 79
5.2.2 Boolean Role Expressions . . . . . . . . . . . . . . . . . . . . . . . 89
6 Transitive Roles and Role Hierarchies 93
6.1 Transitive and Inverse Roles: SI . . . . . . . . . . . . . . . . . . . . . . . . 94
6.1.1 The SI-algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
6.1.2 Blocking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
6.1.3 A Tableau Algorithm for SI . . . . . . . . . . . . . . . . . . . . . . 100
6.1.4 Constructing an SI Tableau . . . . . . . . . . . . . . . . . . . . . . 102
6.1.5 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
6.2 Adding Role Hierarchies and Qualifying Number Restrictions: SHIQ . . . 112
6.2.1 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 113
6.2.2 The Complexity of Reasoning with SHIQ . . . . . . . . . . . . . . . 115
6.3 Practical Reasoning for SHIQ . . . . . . . . . . . . . . . . . . . . . . . . . 121
6.3.1 A SHIQ-Tableau . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
6.3.2 A Tableau Algorithm for SHIQ . . . . . . . . . . . . . . . . . . . . 124
7 Guarded Fragments 137
7.1 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
7.2 Reasoning with Guarded Fragments . . . . . . . . . . . . . . . . . . . . . . 140
7.2.1 Tableau Reasoning for CGF . . . . . . . . . . . . . . . . . . . . . . 141
7.2.2 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
8 Summary 155
Bibliography 159
List of Figures 173