Saturation-Based Decision Procedures for Extensions of the Guarded Fragment [PhD Thesis]

1 Introduction 1
1.1 Description Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Saturation-Based Decision Procedures . . . . . . . . . . . . . . . . . . 3
1.3 The Guarded Fragment and Its Extensions . . . . . . . . . . . . . . . 5
1.4 Theories of Compositional Binary Relations . . . . . . . . . . . . . . 5
1.5 Outline and Structure of this Thesis . . . . . . . . . . . . . . . . . . . 6
1.6 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2 Engineering Logical Algorithms using S.B.T.P. 10
2.1 Description Logic EL . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Resolution-Based Decision Procedures . . . . . . . . . . . . . . . . . 15
2.2.1 The Ordered Resolution Calculus . . . . . . . . . . . . . . . . 16
2.3 A Resolution Decision Procedure for EL . . . . . . . . . . . . . . . . 19
2.3.1 Enforcing Termination . . . . . . . . . . . . . . . . . . . . . . 19
2.3.2 Making It Simple . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.3.3 Complexity Analysis . . . . . . . . . . . . . . . . . . . . . . . 26
2.4 Extensions of DL EL . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.4.1 GCIs, Bottom Concept and Extended Role Hierarchies . . . . 29
2.4.2 Cross-Products of Concepts . . . . . . . . . . . . . . . . . . . 32
2.4.3 Nominals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.5 DL EL and Restricted Role-Value Maps . . . . . . . . . . . . . . . . 35
2.5.1 Undecidability for Some Extensions of EL with Role-Value Maps 35
2.5.2 A Resolution Strategy for EL with Restricted Role-Value Maps 38
2.6 First Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
2.7 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
2.8 Related Works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
3 Preliminaries 53
3.1 Logical Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.1.1 First-Order Logic . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.1.2 First-Order Clause Logic . . . . . . . . . . . . . . . . . . . . . 55
3.1.3 Orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.1.4 Substitutions And Unification . . . . . . . . . . . . . . . . . . 59
3.2 Modal and Description Logics . . . . . . . . . . . . . . . . . . . . . . 61
3.2.1 Propositional Modal Logics . . . . . . . . . . . . . . . . . . . 61
3.2.2 Description Logics . . . . . . . . . . . . . . . . . . . . . . . . 64
3.2.3 Reasoning in Modal and Description Logics . . . . . . . . . . 69
3.3 Decidable Fragments of First-Order Logic . . . . . . . . . . . . . . . 71
3.3.1 Prefix-vocabulary Classes . . . . . . . . . . . . . . . . . . . . 71
3.3.2 Two-Variable Fragments . . . . . . . . . . . . . . . . . . . . . 73
3.3.3 Guarded Fragments . . . . . . . . . . . . . . . . . . . . . . . . 74
3.4 Domino Problems and Undecidability . . . . . . . . . . . . . . . . . . 76
3.5 A Framework of Saturation-Based Theorem Proving . . . . . . . . . . 77
3.5.1 Saturation-Based Theorem Proving . . . . . . . . . . . . . . . 77
3.5.2 The Ordered Resolution Calculus . . . . . . . . . . . . . . . . 78
3.5.3 Equational Reasoning . . . . . . . . . . . . . . . . . . . . . . 80
3.5.4 Chaining Calculi . . . . . . . . . . . . . . . . . . . . . . . . . 82
3.5.5 Variations of Inference Systems . . . . . . . . . . . . . . . . . 87
3.5.6 The Theorem Proving Process . . . . . . . . . . . . . . . . . . 89
3.5.7 Clause Normal Form Transformation . . . . . . . . . . . . . . 92
4 Saturation-Based Decision Procedures 97
4.1 Decision Procedures Based on Ordered Resolution . . . . . . . . . . . 99
4.1.1 Deciding the Guarded Fragment without Equality . . . . . . . 99
4.1.2 Deciding the Two-Variable Fragment without Equality . . . . 108
4.1.3 Deciding the Monadic Fragments without Equality . . . . . . 114
4.2 Combinations of Decidable Fragments . . . . . . . . . . . . . . . . . . 118
4.2.1 Deciding the Combination of Guarded and Two-Variable Fragments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
4.2.2 Deciding Combinations with the Monadic Fragment . . . . . . 124
4.2.3 Undecidability Results . . . . . . . . . . . . . . . . . . . . . . 126
4.3 Paramodulation-based Decision Procedures . . . . . . . . . . . . . . . 127
4.3.1 Guarded Fragment with Equality . . . . . . . . . . . . . . . . 127
4.3.2 Guarded Fragment with Constants . . . . . . . . . . . . . . . 130
4.3.3 Guarded Fragment and Functionality . . . . . . . . . . . . . . 137
4.3.4 Guarded Fragment with Counting . . . . . . . . . . . . . . . . 145
4.4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149
5 Guarded Fragment over Compositional Theories 152
5.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
5.1.1 Examples and Applications of Compositional Theories . . . . 153
5.1.2 A Short History of the Guarded Fragment with Transitivity . 160
5.1.3 Undecidability of the Guarded Fragment with Transitivity . . 161
5.1.4 On the Modal Fragment with Transitivity . . . . . . . . . . . 165
5.2 Extensions without Equality . . . . . . . . . . . . . . . . . . . . . . . 169
5.2.1 Deciding the Guarded Fragment with Transitive Guards . . . 169
5.2.2 Deciding the Guarded Fragment with Compositional Guards . 177
5.2.3 Undecidability of the Guarded Fragment over Relational Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183
5.3 Extensions with Equality . . . . . . . . . . . . . . . . . . . . . . . . . 185
5.3.1 Undecidability for Associative Compositional Axioms . . . . . 185
5.3.2 Undecidability for Conjunctions of Transitive Guards . . . . . 187
5.3.3 A Decision Procedure for the Guarded Fragment with Tran-
sitive Guards and Equality . . . . . . . . . . . . . . . . . . . . 188
5.4 Conclusions and Future Works . . . . . . . . . . . . . . . . . . . . . . 189
6 Summary 192
A DL EL and Its Extensions 196
A.1 Evaluation of Queries in DL EL Using Ordered Resolution . . . . . . 196
A.2 An Example for Query Evaluation in DL EL Using Datalog . . . . . 199
A.3 Additional Rules for Querying Subsumption in DL EL . . . . . . . . 201
A.4 Extensions of DL EL with Cross-Products of Concepts . . . . . . . . 203
A.5 Extensions of DL EL with Nominals . . . . . . . . . . . . . . . . . . 208
A.6 Extensions of DL EL with Restricted Role-Value Maps . . . . . . . . 217
A.7 Prolog Programs for Reasoning in DL EL . . . . . . . . . . . . . . . . 221
B Schemes of Expressions and Clauses 226
B.1 Signature Parameters and the Choice Operator . . . . . . . . . . . . 227
B.2 Sets of Terms and Literals . . . . . . . . . . . . . . . . . . . . . . . . 228
B.3 Variable-Vectors and Scheme definitions . . . . . . . . . . . . . . . . 229
B.4 The Formal Semantics for Clause Schemes . . . . . . . . . . . . . . . 231
B.5 Scheme Contexts and Defined Parameters . . . . . . . . . . . . . . . 233
B.6 Indexing of Signature Elements and Parameters . . . . . . . . . . . . 234
B.7 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 235
C Complexity of Saturation-Based Decision Procedures 236
C.1 Resolution-Based Decision Procedures . . . . . . . . . . . . . . . . . 236
C.1.1 Complexity of the Procedure for GF . . . . . . . . . . . . . . 236
C.1.2 Complexity of the Procedure for FO2 . . . . . . . . . . . . . . 240
C.1.3 Complexity of the Procedure for Mf . . . . . . . . . . . . . . 242
C.2 Paramodulation-Based Decision Procedures . . . . . . . . . . . . . . 243
C.2.1 Complexity of the Procedure for GF≃ . . . . . . . . . . . . . . 243
C.2.2 Complexity of the Procedure for GF≃ with Constants . . . . . 244
D GF with Compositional Guards 246
D.1 Redundancy Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . 246
D.2 Deciding GF[TG] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 250
D.3 Deciding GF[CG] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 253
D.4 A Sketch of a Decision Procedure for GF≃[TG] . . . . . . . . . . . . . 256
Bibliography 265
Index 278