product iamge

Decidability of Modal Logics with Particular Emphasis on the Interval Temporal Logics [PhD Thesis]

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Download
Search on Amazon

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

Author(s): Jakub Michaliszyn
Publisher: University of Wroclaw
Year: 2012

Language: English
Pages: 100

I. Introduction 1
1. Modal logic 3
2. Halpern{Shoham logic 5
II. Elementary modal logics 7
3. Overview 9
4. Preliminaries 11
4.1. Domino systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
5. Undecidability 14
5.1. Key tool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
5.2. First-order formulas with three variables . . . . . . . . . . . . . . . . 16
5.3. Undecidability for unimodal logic dened by Horn formulas with inequality
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
5.4. Undecidability for bimodal logic defined by Horn formulas . . . . . . 19
5.5. Local satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
6. Model properties 22
6.1. Minimal tree-based models . . . . . . . . . . . . . . . . . . . . . . . 22
6.2. Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
6.3. The closures of linear structures . . . . . . . . . . . . . . . . . . . . . 24
6.4. Forks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
6.5. Boundedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
6.6. Omitted proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
6.6.1. Proof of Lemma 6.2 . . . . . . . . . . . . . . . . . . . . . . . 26
6.6.2. Proof of Lemma 6.9 . . . . . . . . . . . . . . . . . . . . . . . 28
6.6.3. Proof of Lemma 6.10 . . . . . . . . . . . . . . . . . . . . . . . 32
6.6.4. Proof of Lemma 6.11 . . . . . . . . . . . . . . . . . . . . . . . 34
6.6.5. Proof of Lemma 6.12 . . . . . . . . . . . . . . . . . . . . . . . 35
7. The decidability 40
7.1. Tree-compatible case . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
7.1.1. Formulas that do not force long edges . . . . . . . . . . . . . 40
7.1.2. Formulas that force only long forward edges . . . . . . . . . . 41
7.1.3. Formulas that force long and backward edges . . . . . . . . . 42
7.2. The tree-incompatibility . . . . . . . . . . . . . . . . . . . . . . . . . 42
7.3. Sharpening the complexity . . . . . . . . . . . . . . . . . . . . . . . . 43
7.3.1. Formulas with TCMP . . . . . . . . . . . . . . . . . . . . . . 43
7.3.2. Formulas without TCMP that do not force long edges . . . . 45
7.3.3. Formulas without TCMP that force only long forward edges . 46
7.3.4. Formulas without TCMP that force long and backward edges 47
7.4. Horn formulas and equality . . . . . . . . . . . . . . . . . . . . . . . 48
8. Finite satisfiability 49
8.1. Formulas that do not force long edges . . . . . . . . . . . . . . . . . 49
8.1.1. Local satisfiability . . . . . . . . . . . . . . . . . . . . . . . . 49
8.1.2. Global satisfiability . . . . . . . . . . . . . . . . . . . . . . . . 50
8.2. Formulas that force long edges . . . . . . . . . . . . . . . . . . . . . 59
III. Halpern{Shoham logic 61
9. Overview 63
9.1. Main theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
9.2. Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
10.Proof of Theorem 9.1 66
10.1. The Regular Language LA . . . . . . . . . . . . . . . . . . . . . . . . 66
10.2. Orientation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
10.3. Encoding a Finite Automaton . . . . . . . . . . . . . . . . . . . . . . 71
10.4. A Cloud . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
10.5. Using a cloud. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
10.5.1. An example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
10.5.2. Encoding two-counter automaton . . . . . . . . . . . . . . . . 75
11.Proof of Theorem 9.2 76
11.1. Damage assessment . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
11.2. The parabola . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
12.More results 81
12.1. Superinterval relation . . . . . . . . . . . . . . . . . . . . . . . . . . 81
12.2. Global satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
12.3. Strict D . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
12.4. Arbitrary orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84