This book is an introduction to finite model theory which stresses the computer science origins of the area. In addition to presenting the main techniques for analyzing logics over finite models, the book deals extensively with applications in databases, complexity theory, and formal languages, as well as other branches of computer science. It covers Ehrenfeucht-Fraïssé games, locality-based techniques, complexity analysis of logics, including the basics of descriptive complexity, second-order logic and its fragments, connections with finite automata, fixed point logics, finite variable logics, zero-one laws, and embedded finite models, and gives a brief tour of recently discovered applications of finite model theory.
This book can be used both as an introduction to the subject, suitable for a one- or two-semester graduate course, or as reference for researchers who apply techniques from logic in computer science.
Author(s): Leonid Libkin
Series: Texts in Theoretical Computer Science. An EATCS Series
Publisher: Springer
Year: 2004
Language: English
Pages: 320
Leonid Libkin - Elements of Finite Model Theory (2004) ......Page 1
Preface ......Page 7
Contents ......Page 10
1.1 A Database Example ......Page 14
1.2 An Example from Complexity Theory ......Page 17
1.3 An Example from Formal Language Theory ......Page 19
1.4 An Overview of the Book ......Page 21
1.5 Exercises ......Page 23
2.1 Background from Mathematical Logic ......Page 25
2.2 Background from Automata and Computability Theory ......Page 29
2.3 Background from Complexity Theory ......Page 31
2.4 Bibliographic Notes ......Page 33
3.1 First Inexpressibility Proofs ......Page 34
3.2 Definition and Examples of Ehrenfeucht-Fraïssé Games ......Page 37
3.3 Games and the Expressive Power of FO ......Page 43
3.4 Rank-k Types ......Page 44
3.5 Proof of the Ehrenfeucht-Fraïssé Theorem ......Page 46
3.6 More Inexpressibility Results ......Page 48
3.7 Bibliographic Notes ......Page 51
3.8 Exercises ......Page 52
4.1 Neighborhoods, Hanf-locality, and Gaifman-locality ......Page 55
4.2 Combinatorics of Neighborhoods ......Page 59
4.3 Locality of FO ......Page 61
4.4 Structures of Small Degree ......Page 64
4.5 Locality of FO Revisited ......Page 67
4.6 Bibliographic Notes ......Page 72
4.7 Exercises ......Page 73
5.1 Invariant Queries ......Page 76
5.2 The Power of Order-invariant FO ......Page 78
5.3 Locality of Order-invariant FO ......Page 82
5.5 Exercises ......Page 92
6.1 Data, Expression, and Combined Complexity ......Page 95
6.2 Circuits and FO Queries ......Page 97
6.3 Expressive Power with Arbitrary Predicates ......Page 101
6.4 Uniformity and AC0 ......Page 103
6.6 Parametric Complexity and Locality ......Page 107
6.7 Conjunctive Queries ......Page 110
6.8 Bibliographic Notes ......Page 116
6.9 Exercises ......Page 117
7.1 Second-Order Logic and Its Fragments ......Page 120
7.2 MSO Games and Types ......Page 123
7.3 Existential and Universal MSO on Graphs ......Page 126
7.4 MSO on Strings and Regular Languages ......Page 131
7.5 FO on Strings and Star-Free Languages ......Page 134
7.6 Tree Automata ......Page 136
7.7 Complexity of MSO ......Page 140
7.8 Bibliographic Notes ......Page 143
7.9 Exercises ......Page 144
8.1 Counting and Unary Quantihers ......Page 148
8.2 An Infinit ary Counting Logic ......Page 152
8.3 Games for L*∞ω(Cnt) ......Page 158
8.4 Counting and Locality ......Page 160
8.5 Complexity of Counting Quantifiers ......Page 162
8.6 Aggregate Operators ......Page 165
8.8 Exercises ......Page 168
9.1 Trakhtenbrot’s Theorem and Failure of Completeness ......Page 171
9.2 Fagin’s Theorem and NP ......Page 174
9.4 Exercises ......Page 180
10 Fixed Point Logics and Complexity Classes ......Page 183
10.1 Fixed Points of Operators on Sets ......Page 184
10.2 Fixed Point Logics ......Page 186
10.3 Properties of LFP and IFP ......Page 190
10.4 LFP, PFP, and Polynomial Time and Space ......Page 198
10.5 Datalog and LFP ......Page 201
10.6 Transitive Closure Logic ......Page 205
10.7 A Logic for PTime? ......Page 210
10.8 Bibliographic Notes ......Page 212
10.9 Exercises ......Page 213
11.1 Logics with Finitely Many Variables ......Page 217
11.2 Pebble Games ......Page 221
11.3 Definability of Types ......Page 226
11.4 Ordering of Types ......Page 231
11.5 Canonical Structures and the Abiteboul-Vianu Theorem ......Page 235
11.6 Bibliographic Notes ......Page 238
11.7 Exercises ......Page 239
12.1 Asymptotic Probabilities and Zero-One Laws ......Page 241
12.2 Extension Axioms ......Page 244
12.3 The Random Graph ......Page 247
12.4 Zero-One Law and Second-Order Logic ......Page 249
12.5 Almost Everywhere Equivalence of Logics ......Page 251
12.6 Bibliographic Notes ......Page 252
12.7 Exercises ......Page 253
13.1 Embedded Finite Models: the Setting ......Page 255
13.2 Analyzing Embedded Finite Models ......Page 258
13.3 Active-Generic Collapse ......Page 262
13.4 Restricted Quantifier Collapse ......Page 266
13.5 The Random Graph and Collapse to MSO ......Page 271
13.6 An Application: Constraint Databases ......Page 273
13.7 Bibliographic Notes ......Page 276
13.8 Exercises ......Page 277
14.1 Finite Model Property and Decision Problems ......Page 280
14.2 Temporal and Modal Logics ......Page 283
14.3 Constraint Satisfaction and Homomorphisms of Finite Models ......Page 290
14.4 Bibliographic Notes ......Page 293
References ......Page 295
List of Notation ......Page 308
Index ......Page 310
Name Index ......Page 316