Many-Dimensional Modal Logics: Theory and Applications (eBook)

Front Cover 1
Many-Dimensional Modal Logics: Theory and Applications 4
Copyright Page 5
Contents 16
Part I: Introduction 20
Chapter 1. Modal logic basics 22
1.1 Modal axiomatic systems 22
1.2 Possible world semantics 28
1.3 Classical first-order logic and the standard translation 34
1.4 Multimodal logics 39
1.5 Algebraic semantics 46
1.6 Decision, complexity and axiomatizability problems 50
Chapter 2. Applied modal logic 60
2.1 Temporal logic 60
2.2 Interval temporal logic 68
2.3 Epistemic logic 74
2.4 Dynamic logic 80
2.5 Description logic 84
2.6 Spatial logic 97
2.7 Intuitionistic logic 111
2.8 'Model level' reductions between logics 115
Chapter 3. Many-dimensional modal logics 130
3.1 Fusions 130
3.2 Spatio-temporal logics 133
3.3 Products 144
3.4 Temporal epistemic logics 153
3.5 Classical first-order logic as a propositional multimodal logic 160
3.6 First-order modal logics 162
3.7 First-order temporal logics 176
3.8 Description logics with modal operators 183
3.9 HS as a two-dimensional logic 198
3.10 Modal transition logics 199
3.11 Intuitionistic modal logics 206
Part II: Fusions and products 214
Chapter 4. Fusions of modal logics 216
4.1 Preserving Kripke completeness and the finite model property 216
4.2 Algebraic preliminaries 219
4.3 Preserving decidability of global consequence 224
4.4 Preserving decidability 227
4.5 Preserving interpolation 235
4.6 On the computational complexity of fusions 237
Chapter 5. Products of modal logics: introduction 240
5.1 Axiomatizing products 241
5.2 Proving decidability with quasimodels 254
5.3 The finite model property 263
5.4 Proving undecidability 271
5.5 Proving complexity with tilings 281
Chapter 6. Decidable products 292
6.1 Warming up: Kn x Km 293
6.2 CPDL x Km 304
6.3 Products of epistemic logics with Km 316
6.4 Products of temporal logics with Km 322
6.5 Products with S5 338
6.6 Products with multimodal S5 353
Chapter 7. Undecidable products 362
7.1 Products of linear orders with infinite ascending chains 363
7.2 Products of linear orders with infinite descending chains 373
7.3 Products of Dedekind complete linear orders 380
7.4 Products of finite linear orders 383
7.5 More undecidable products 386
Chapter 8. Higher-dimensional products 396
8.1 S5 x S5 x ... x S5 398
8.2 Products between K4n and S5n 410
8.3 Products with the fmp 413
8.4 Between Kn and SSn 415
8.5 Finitely axiomatizable and decidable products 429
Chapter 9. Variations on products 436
9.1 Relativized products 437
9.2 Valuation restrictions 453
Chapter 10. Intuitionistic modal logics 458
10.1 Intuitionistic modal logics with D 458
10.2 Intuitionistic modal logics with D and dimond 464
10.3 The finite model property 472
Part III: First-order modal logics 480
Chapter 11. Fragments of first-order temporal logics 484
11.1 Undecidable fragments 484
11.2 Monodic formulas, decidable fragments 490
11.3 Embedding into monadic second-order theories 500
11.4 Complexity of decidable fragments of QLogsu(N) and their complexity 507
11.5 Satisfiability in models over (N, < ) with finite domains
11.6 Satisfiability in models over {R< } with finite domains
11.7 Axiomatizing monodic fragments 546
11.8 Monodicity and equality 557
Chapter 12. Fragments of first-order dynamic and epistemic logics 566
12.1 Decision problems 566
12.2 Axiomatizing monodic fragments 569
Part IV: Applications to knowledge representation 584
Chapter 13. Temporal epistemic logics 586
13.1 Synchronous systems 588
13.2 Agents who know the time and neither forget nor learn 594
Chapter 14. Modal description logics 602
14.1 Concept satisfiability 604
14.2 General formula satisfiability 610
14.3 Restricted formula satisfiability 624
14.4 Satisfiability in models with finite domains 629
Chapter 15. Tableaux for modal description logics 634
15.1 Tableaux for ALC 635
15.2 Tableaux for KALC with constant domains 642
15.3 Adding expressive power to KALC 659
Chapter 16. Spatio-temporal logics 666
16.1 Modal formalisms for spatio-temporal reasoning 667
16.2 Embedding spatio-temporal logics in first-order temporal logic 673
16.3 Complexity of spatio-temporal logics 680
16.4 Models based on Euclidean spaces 691
Epilogue 698
Bibliography 704
List of tables 744
List of languages and logics 746
Symbol index 752
Subject index 756