Unrestricted and finite model reasoning in class-based representation formalisms [PhD Thesis]

1 Representing Structured Information 1
1.1 Semantic Networks and Frame Based Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.2 Description Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Semantic Data Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.4 Object-Oriented Data Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.5 Goal of the Thesis and Main Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.6 Structure of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2 Representing Intensional Knowledge by L-Schemata 9
2.1 Syntax and Semantics of L-Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.1.1 The Core Language (L0, L−) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.1.2 Disjunction (LU) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.1.3 Qualified Existential Quantification (LE) . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.1.4 Number Restrictions (LN, LF, LQ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.1.5 Inverse Attributes (LI) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.1.6 General Negation (LC) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.1.7 Arbitrary Links (LL, LD, LC, LV) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.1.8 Structured Objects (LO) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.1.9 Achieving Maximum Expressivity (LT , LT −) . . . . . . . . . . . . . . . . . . . . . . . 17
2.1.10 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2 L-Schemata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.2.1 Cycles in L-Schemata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.2.2 Primitive L-Schemata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.2.3 Free L-Schemata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.2.4 Summary and Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.3 Schema Level Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.3.1 Reasoning Services . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.3.2 Equivalence of Schemata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.4 Finite versus Unrestricted Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3 Modeling Known Formalisms 29
3.1 Comparison with Description Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2 Modeling Frame Based Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3.2.1 Syntax of Frame Based Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3.2.2 Semantics of Frame Based Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.2.3 Relationship between Frame Based Systems and L-Schemata . . . . . . . . . . . . . . 32
3.3 Modeling Semantic Data Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.3.1 Syntax of the Entity-Relationship Model . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.3.2 Semantics of the Entity-Relationship Model . . . . . . . . . . . . . . . . . . . . . . . . 36
3.3.3 Relationship between ER-Schemata and L-Schemata . . . . . . . . . . . . . . . . . . . 37
3.4 Modeling Object-Oriented Data Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.4.1 Syntax of an Object-Oriented Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.4.2 Semantics of an Object-Oriented Model . . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.4.3 Relationship between Object-Oriented Schemata and L-Schemata . . . . . . . . . . . 43
4 Intrinsic Complexity of Reasoning 45
4.1 Complexity Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4.1.1 Complete Problems for Complexity Classes . . . . . . . . . . . . . . . . . . . . . . . . 46
4.2 Lower Bounds by Direct Reductions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4.2.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
4.2.2 Acyclic Primitive L0-Schemata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
4.2.3 Acyclic Primitive LU-Schemata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
4.2.4 General Primitive L0-Schemata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.3 Eliminating Qualified Existential Quantification . . . . . . . . . . . . . . . . . . . . . . . . . . 60
4.4 Undecidable L-Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
4.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5 Unrestricted Model Reasoning 67
5.1 Unrestricted Model Reasoning on Primitive LUNI-Schemata . . . . . . . . . . . . . . . . . . 67
5.1.1 Relaxation of a Schema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
5.1.2 Two-Way Deterministic Tree Structures . . . . . . . . . . . . . . . . . . . . . . . . . . 69
5.1.3 Expansion of Two Way Deterministic Tree Structures . . . . . . . . . . . . . . . . . . 71
5.1.4 Upper Bounds for Unrestricted Model Reasoning . . . . . . . . . . . . . . . . . . . . . 75
5.2 Unrestricted Model Reasoning on Free LT −-Schemata . . . . . . . . . . . . . . . . . . . . . . 76
5.2.1 Reduction from LT − to LCQIL¢ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
5.2.2 Reduction from LCQIL¢ to LCFIL¢ . . . . . . . . . . . . . . . . . . . . . . . . . . 81
5.2.3 Decidability of LCFIL¢ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
5.2.4 Upper Bounds for Unrestricted Model Reasoning . . . . . . . . . . . . . . . . . . . . . 86
6 Finite Model Reasoning 87
6.1 Systems of Linear Inequalities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
6.1.1 Acceptable Solutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
6.2 Finite Model Reasoning on Primitive LUNI-Schemata . . . . . . . . . . . . . . . . . . . . . . 90
6.2.1 Normalization of a Schema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
6.2.2 Expansion of a Schema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
6.2.3 System of Inequalities Corresponding to a Schema . . . . . . . . . . . . . . . . . . . . 95
6.2.4 Characterization of Finite Class Consistency . . . . . . . . . . . . . . . . . . . . . . . 96
6.2.5 Upper Bounds for Finite Model Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . 101
6.3 Towards an Efficient Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
6.3.1 Strategies for Constructing the Expansion . . . . . . . . . . . . . . . . . . . . . . . . . 103
6.3.2 Special Cases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
6.4 Finite Model Reasoning on Free LCNI-Schemata . . . . . . . . . . . . . . . . . . . . . . . . . 106
6.4.1 Normalization of a Schema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
6.4.2 Expansion of a Schema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
6.4.3 Biexpansion of a Schema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
6.4.4 System of Inequalities Corresponding to a Schema . . . . . . . . . . . . . . . . . . . . 114
6.4.5 Characterization of Finite Class Consistency . . . . . . . . . . . . . . . . . . . . . . . 115
6.4.6 Upper Bounds for Finite Model Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . 119
6.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
A Finite Automata on Infinite Objects 121
A.1 Sequential Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
A.2 Tree Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
B Propositional Dynamic Logics 125
B.1 Syntax and Semantics of PDLs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
B.2 The Correspondence between L-Languages and PDLs . . . . . . . . . . . . . . . . . . . . . . 126
B.3 Extensions and Variants of PDLs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127
B.3.1 Extensions of cpdl (rcpdl, qcpdl, fcpdl) . . . . . . . . . . . . . . . . . . . . . . . 127
B.3.2 Variants of PDLs Described by Automata (APDLs) . . . . . . . . . . . . . . . . . . . 128
B.4 Additional Notions about PDLs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129
B.4.1 Fischer-Ladner Closure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129
B.4.2 Tree Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129
Bibliography 131
List of Publications 141