β Scribed by Gaelle Fontaine
No coin nor oath required. For personal study only.
1 Introduction 1
2 Preliminaries 11
2.1 Syntax of the -calculus . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Semantics for the -calculus . . . . . . . . . . . . . . . . . . . . . 15
2.3 Game terminology and the evaluation game . . . . . . . . . . . . 21
2.4 -Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.4.1 !-Automata . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.4.2 -automata . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.4.3 Disjunctive formulas . . . . . . . . . . . . . . . . . . . . . 31
2.5 Axiomatization of the -calculus . . . . . . . . . . . . . . . . . . . 32
2.6 Expressivity of the -calculus . . . . . . . . . . . . . . . . . . . . 33
2.6.1 Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.6.2 Expressivity results . . . . . . . . . . . . . . . . . . . . . . 35
2.6.3 Expressivity results for -programs . . . . . . . . . . . . . 39
2.7 Graded -calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3 Completeness for the -calculus on nite trees 45
3.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.2 Rank of a formula . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.3 Completeness for generalized models . . . . . . . . . . . . . . . . 50
3.4 Completeness for nite trees . . . . . . . . . . . . . . . . . . . . . 55
3.5 Adding shallow axioms to K + x:2x . . . . . . . . . . . . . . . 58
3.6 Graded -calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
3.7 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
4 The -calculus and frame de nability on trees 67
4.1 MLF-de nability on trees . . . . . . . . . . . . . . . . . . . . . . 69
4.2 Graded -calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
4.3 Preservation under p-morphic images . . . . . . . . . . . . . . . . 84
4.4 Local de nability . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
4.5 Negative and projective de nability . . . . . . . . . . . . . . . . . 108
4.5.1 Negative de nability . . . . . . . . . . . . . . . . . . . . . 108
4.5.2 Projective de nability . . . . . . . . . . . . . . . . . . . . 110
4.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
5 Characterizations of fragments of the -calculus 115
5.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
5.1.1 Structures and games . . . . . . . . . . . . . . . . . . . . . 117
5.1.2 Guarded and disjunctive formulas . . . . . . . . . . . . . . 118
5.1.3 Expansion of a formula . . . . . . . . . . . . . . . . . . . . 119
5.1.4 Monotonicity and positivity . . . . . . . . . . . . . . . . . 120
5.2 Finite path property . . . . . . . . . . . . . . . . . . . . . . . . . 122
5.3 Finite width property . . . . . . . . . . . . . . . . . . . . . . . . . 129
5.4 Continuity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
5.4.1 Link with Scott continuity . . . . . . . . . . . . . . . . . . 139
5.4.2 Constructivity . . . . . . . . . . . . . . . . . . . . . . . . . 140
5.4.3 Semantic characterization of continuity . . . . . . . . . . . 141
5.5 Complete additivity . . . . . . . . . . . . . . . . . . . . . . . . . . 144
5.6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163
6 CoreXPath restricted to the descendant relation 165
6.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
6.1.1 XML trees . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
6.1.2 CoreXPath, the navigational core of XPath 1.0 . . . . . . 167
6.1.3 Connections with modal logic . . . . . . . . . . . . . . . . 169
6.2 CoreXPath(#+) node expressions . . . . . . . . . . . . . . . . . . 171
6.3 CoreXPath(#+) path expressions . . . . . . . . . . . . . . . . . . 179
6.4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187
7 Automata for coalgebras: an approach using predicate liftings 189
7.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191
7.1.1 Coalgebras . . . . . . . . . . . . . . . . . . . . . . . . . . . 191
7.1.2 Graph games . . . . . . . . . . . . . . . . . . . . . . . . . 194
7.2 Automata for the coalgebraic -calculus . . . . . . . . . . . . . . 197
7.3 Finite model property . . . . . . . . . . . . . . . . . . . . . . . . 203
7.4 One-step tableau completeness . . . . . . . . . . . . . . . . . . . . 214
7.5 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222
8 Conclusion 223
Bibliography 227
Index 237
List of symbols 241
Samenvatting 243
Abstract 245
π SIMILAR VOLUMES
This dissertation is about extending modal logic. It tells you what a system of extended modal logic is, it gives you three case studies of systems of modal logic, and it gives you very general approaches to two important themes in modal logic.
This dissertation is about extending modal logic. It tells you what a system of extended modal logic is, it gives you three case studies of systems of modal logic, and it gives you very general approaches to two important themes in modal logic.
This is a PhD Thesis written under supervision of Prof.dr. J.A.G. Groenendijk and Prof.dr. J.F.A.K. van Benthem at the Institute for Logic, Language and Computation.
This is a doctoral dissertation of Edith Spaan under the supervision of prof. Johan van Benthem.
This is a doctoral dissertation of Yde Venema under the supervision of prof. Johan van Benthem.
In this thesis we investigate modal logics from a lattice theoretic point of view. There are essentially two well-known methods of research on lattices of modal logics. The investigation of the lattice of modal logics as a whole, and the local investigation of the lattice of extensions of some stron