Finite model theory and its applications / Erich Grädel ... [and others].

Format:

Book

Contributor:

Grädel, Erich, 1958-

Class of 1924 Book Fund.

Series:

Texts in theoretical computer science

Texts in theoretical computer science, 1862-4499

Language:

English

Subjects (All):

Finite model theory.

Computational complexity.

Constraint databases.

Physical Description:

xi, 437 pages : illustrations ; 24 cm.

Place of Publication:

Berlin ; New York : Springer, [2007]

Summary:

This book gives a comprehensive overview of central topics in finite model theory - expressive power of logics, descriptive complexity, and zero-one laws - together with selected applications relating to database theory and artificial intelligence, especially constraint databases and constraint satisfaction problems. The final chapter provides a concise modern introduction to modal logic, emphasizing the interaction with finite model theory. The underlying theme of the book is the use of first-order, second-order, fixed-point, and infinitary logic, as well as various fragments of and hierarchies within these logics, to gain insight into phenomena and problems in complexity theory and combinatorics.

The book emphasizes the use of combinatorial games, such as extensions and refinements of the Ehrenfeucht-Fraisse games, as a powerful way to analyze the expressive power of logics, and illustrates how sophisticated notions from model theory and combinatorics, such as o-minimality and treewidth, arise naturally in the applications of finite model theory to database theory and artificial intelligence. Students of logic and computer science will find here the tools necessary to embark on research into finite model theory, and all readers will experience the excitement of a vibrant area of the applications of logic to computer science.

Contents:

1 Unifying Themes in Finite Model Theory 1

1.1 Definability Theory 2

1.1.1 Classification of Concepts in Terms of Definitional Complexity 2

1.1.2 What More Do We Know When We Know a Concept Is L-Definable? 4

1.1.3 Logics with Finitely Many Variables 7

1.1.4 Distinguishing Structures: L-Equivalence and Comparison Games 8

1.1.5 Random Graphs and 0-1 Laws 10

1.1.6 Constraint Satisfaction Problems 11

1.2 Descriptive Complexity 12

1.2.1 Satisfaction 13

1.2.2 What Is a Logic for PTIME? 16

1.3 Finite Model Theory and Infinite Structures 18

1.4 Tame Fragments and Tame Classes 20

2 On the Expressive Power of Logics on Finite Models 27

2.3 Ehrenfeucht-Fraisse Games for First-Order Logic 34

2.4 Computational Complexity 50

2.4.1 Complexity Classes 50

2.4.2 The Complexity of Logic 51

2.5 Ehrenfeucht-Fraisse Games for Existential Second-Order Logic 54

2.6 Logics with Fixed-Point Operators 59

2.6.1 Operators and Fixed Points 60

2.6.2 Least Fixed-Point Logic 64

2.6.3 Datalog and Datalog([NotEqual]) 74

2.6.4 The Complementation Problem for LFP[subscript 1] and a Normal Form for LFP 79

2.6.5 Partial Fixed-Point Logic 82

2.7 Infinitary Logics with Finitely Many Variables 86

2.7.1 The Infinitary Logic L[Characters not reproducible] 87

2.7.2 Pebble Games and L[Characters not reproducible]-Definability 89

2.7.3 0-1 Laws for L[Characters not reproducible] 97

2.7.4 Definability and Complexity of L[Characters not reproducible]-Equivalence 99

2.7.5 Least Fixed-Point Logic vs. Partial Fixed-Point Logic on Finite Structures 104

2.8 Existential Infinitary Logics with Finitely Many Variables 106

2.8.1 The Infinitary Logics [Characters not reproducible] and [Characters not reproducible] ([NotEqual]) 107

2.8.2 Existential Pebble Games 109

2.8.3 Descriptive Complexity of Fixed Subgraph Homeomorphism Queries 116

3 Finite Model Theory and Descriptive Complexity 125

3.1 Definability and Complexity 125

3.1.1 Complexity Issues in Logic 126

3.1.2 Model Checking for First-Order Logic 128

3.1.3 The Strategy Problem for Finite Games 129

3.1.4 Complexity of First-Order Model Checking 132

3.1.5 Encoding Finite Structures by Words 135

3.2 Capturing Complexity Classes 138

3.2.1 Capturing NP: Fagin's Theorem 138

3.2.2 Logics That Capture Complexity Classes 144

3.2.3 Capturing Polynomial Time on Ordered Structures 145

3.2.4 Capturing Logarithmic Space Complexity 149

3.2.5 Transitive Closure Logics 151

3.3 Fixed-Point Logics 152

3.3.1 Some Fixed-Point Theory 153

3.3.2 Least Fixed-Point Logic 155

3.3.3 The Modal [mu]-Calculus 157

3.3.4 Parity Games 160

3.3.5 Model-Checking Games for Least Fixed-Point Logic 165

3.3.6 Definability of Winning Regions in Parity Games 169

3.3.7 Simultaneous Fixed-Point Inductions 170

3.3.8 Inflationary Fixed-Point Logic 174

3.3.9 Partial Fixed-Point Logic 177

3.3.10 Datalog and Stratified Datalog 180

3.4 Logics with Counting 186

3.4.1 Logics with Counting Terms 187

3.4.2 Fixed-Point Logic with Counting 188

3.4.3 Datalog with Counting 190

3.5 Capturing PTIME via Canonization 193

3.5.1 Definable Linear Orders 193

3.5.2 Canonizations and Interpretations 194

3.5.3 Capturing PTIME up to Bisimulation 198

3.5.4 Is There a Logic for PTIME? 203

3.6 Algorithmic Model Theory 205

3.6.1 Beyond Finite Structures 205

3.6.2 Finitely Presentable Structures 206

3.6.3 Metafinite Structures 210

3.6.4 Metafinite Spectra 213

3.6.5 Descriptive Complexity over the Real Numbers 216

3.7 Appendix: Alternating Complexity Classes 222

4 Logic and Random Structures 231

4.1 An Instructive Example 231

4.2 Random Graphs 234

4.3 Extension Statements 235

4.4 Closure 237

4.5 The Almost Sure Theory 239

4.6 The Case p Constant 241

4.7 Countable Models 242

4.8 A Dynamic View 243

4.9 Infinite Spectra via Almost Sure Encoding 244

4.10 The Jump Condition 246

4.11 The Complexity Condition 247

4.12 Nonconvergence via Almost Sure Encoding 249

4.13 No Almost Sure Representation of Evenness 251

4.14 The Ehrenfeucht Game 253

4.15 About the References 254

5 Embedded Finite Models and Constraint Databases 257

5.1.1 Organization 258

5.2 Relational Databases and Embedded Finite Models 258

5.3 Constraint Databases 262

5.4 Collapse and Genericity: An Overview 266

5.4.1 Approaches to Proving Expressivity Bounds 267

5.5 Active-Generic Collapse 269

5.5.1 The Ramsey Property 269

5.5.2 Collapse Results 272

5.6 Natural-Active Collapse 273

5.6.1 Collapse: Failure and Success 274

5.6.2 Good Structures vs. Bad Structures: O-minimality 276

5.6.3 Collapse Theorem and Corollaries 277

5.6.4 Collapse Algorithm: the Linear Case 278

5.6.5 Collapse Algorithm: the General Case 280

5.6.6 Collapse Without O-minimality 285

5.6.7 Natural-Generic Collapse 287

5.7 Model Theory and Collapse Results 288

5.7.1 Pseudo-finite Homogeneity 289

5.7.2 Finite Cover Property and Collapse 290

5.7.3 Isolation and Collapse 292

5.8 The VC Dimension and Collapse Results 295

5.8.1 Random Graph and Collapse to MSO 298

5.8.2 Complexity Bounds for Generic Queries 299

5.9 Expressiveness of Constraint Query Languages 301

5.9.1 Reductions to the Finite Case 301

5.9.2 Topological Properties 303

5.9.3 Linear vs. Polynomial Constraints 305

5.10 Query Safety 307

5.10.1 Finite and Infinite Query Safety 308

5.10.2 Safe Translations 309

5.10.3 Finite Query Safety: Characterization 311

5.10.4 Infinite Query Safety: Reduction 316

5.10.5 Deciding Safety 319

5.10.6 Dichotomy Theorem for Embedded Finite Models 321

5.11 Database Considerations 322

5.11.1 Aggregate Operators 323

5.11.2 Higher-Order Features 326

6 A Logical Approach to Constraint Satisfaction 339

6.3 The Computational Complexity of Constraint Satisfaction 344

6.4 Nonuniform Constraint Satisfaction 347

6.5 Monotone Monadic SNP and Nonuniform Constraint Satisfaction 350

6.6 Datalog and Nonuniform Constraint Satisfaction 352

6.7 Datalog, Games, and Constraint Satisfaction 355

6.8 Games and Consistency 357

6.9 Uniform Constraint Satisfaction and Bounded Treewidth 362

7 Local Variations on a Loose Theme: Modal Logic and Decidability 371

7.2 Modal Systems and Bisimulations 373

7.3 Basic Modal Logic 378

7.4 Some Variations 389

7.4.1 Neither Locality nor Looseness: Grid Logics 390

7.4.2 Universal Access: K 395

7.4.3 Generalizing Looseness: the Until Operator 397

7.5 Modal Complexity 404

7.5.1 NP and the Polysize Model Property 405

7.5.2 PSPACE and Polynomially Deep Paths 406

7.5.3 EXPTIME and Exponentially Deep Paths 408

7.5.4 NEXPTIME 410

7.6 Modal Logic and First-Order Logic 413

7.6.1 Guarded Fragments 413

7.6.2 Decidability and Complexity 418.

Notes:

Includes bibliographical references and index.

Local Notes:

Acquired for the Penn Libraries with assistance from the Class of 1924 Book Fund.

ISBN:

9783540004288

3540004289

OCLC:

173244312