The finite model theory toolbox of a database theoretician

ABSTRACT

For many years, finite model theory was viewed as the backbone of database theory, and database theory in turn supplied finite model theory with key motivations and problems. By now, finite model theory has built a large arsenal of tools that can easily be used by database theoreticians without going to the basics such as combinatorial games. We survey such tools here, focusing not on how they are proved, but rather on how to apply them, as-is, in various questions that come up in database theory.

REFERENCES

• 1: M. Ajtai. Sigma11 formulae on finite structures. Annals of Pure and Applied Logic, 24 (1983), 1--48.
• 2: Andreas Blass , Yuri Gurevich , Dexter Kozen, A zero-one law for logic with a fixed-point operator, Information and Control, v.67 n.1-3, p.70-90, Oct./Nov./Dec. 1986 [doi>10.1016/S0019-9958(85)80027-9]
• 3: Mikolaj Bojańczyk , Claire David , Anca Muscholl , Thomas Schwentick , Luc Segoufin, Two-variable logic on data trees and XML reasoning, Proceedings of the twenty-fifth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 26-28, 2006, Chicago, IL, USA [doi>10.1145/1142351.1142354]
• 4: A. Chandra and D. Harel. Computable queries for relational databases. Journal of Computer and System Sciences, 21 (1980), 156--178.
• 5: Anuj Dawar , Steven Lindell , Scott Weinstein, Infinitary logic and inductive definability over finite structures, Information and Computation, v.119 n.2, p.160-175, June 1995 [doi>10.1006/inco.1995.1084]
• 6: Guozhu Dong , Leonid Libkin , Limsoon Wong, Local properties of query languages, Theoretical Computer Science, v.239 n.2, p.277-308, May 28, 2000 [doi>10.1016/S0304-3975(99)00223-6]
• 7: H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer-Verlag, 1995.
• 8: R. Fagin. Monadic generalized spectra. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 21 (1975), 89--96.
• 9: R. Fagin. Probabilities on finite models. Journal of Symbolic Logic, 41 (1976), 50--58.
• 10: Ronald Fagin , Larry J. Stockmeyer , Moshe Y. Vardi, On a monadic NP vs monadic co-NP, Information and Computation, v.120 n.1, p.78-92, July 1995 [doi>10.1006/inco.1995.1100]
• 11: Markus Frick , Martin Grohe, The Complexity of First-Order and Monadic Second-Order Logic Revisited, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.215-224, July 22-25, 2002
• 12: H. Gaifman. On local and non-local properties, Proc.Herbrand Symp., Logic Colloquium '81. North-Holland, 1982.
• 13: Georg Gottlob , Christoph Koch, Monadic datalog and the expressive power of languages for Web information extraction, Journal of the ACM (JACM), v.51 n.1, p.74-113, January 2004 [doi>10.1145/962446.962450]
• 14: Erich Grädel , P. G. Kolaitis , L. Libkin , M. Marx , J. Spencer , Moshe Y. Vardi , Y. Venema , Scott Weinstein, Finite Model Theory and Its Applications (Texts in Theoretical Computer Science. An EATCS Series), Springer-Verlag New York, Inc., Secaucus, NJ, 2005
• 15: Martin Grohe, Parameterized complexity for the database theorist, ACM SIGMOD Record, v.31 n.4, December 2002 [doi>10.1145/637411.637428]
• 16: M. Grohe. Logic, graphs, and algorithms. In Logic and Automata -- History and Perspectives, Amsterdam Univ. Press, 2007.
• 17: Martin Grohe , Thomas Schwentick, Locality of order-invariant first-order formulas, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.112-130, July 2000 [doi>10.1145/343369.343386]
• 18: Stéphane Grumbach , Jianwen Su, Queries with arithmetical constraints, Theoretical Computer Science, v.173 n.1, p.151-181, Feb. 1997 [doi>10.1016/S0304-3975(96)00194-6]
• 19: Y. Gurevich. Logic and the challenge of computer science. In Current trends in theoretical computer science, E. Borger, ed., Computer Science Press, 1988, pages 1--57.
• 20: W. Hanf. Model-theoretic methods in the study of elementary logic. In The Theory of Models, North-Holland, 1965, pages 132--145.
• 21: L. Hella, L. Libkin, and J. Nurmonen. Notions of locality and their logical characterizations over finite models. Journal of Symbolic Logic, 64 (1999), 1751--1773.
• 22: Lauri Hella , Leonid Libkin , Juha Nurmonen , Limsoon Wong, Logics with aggregate operators, Journal of the ACM (JACM), v.48 n.4, p.880-907, July 2001 [doi>10.1145/502090.502100]
• 23: Neil Immerman, Relational queries computable in polynomial time, Information and Control, v.68 n.1-3, p.86-104, Jan/Feb/March 1986 [doi>10.1016/S0019-9958(86)80029-8]
• 24: N. Immerman. Descriptive Complexity. Springer, 1998.
• 25: N. Immerman and E. Lander. Describing graphs: a first order approach to graph canonization. In Complexity Theory Retrospective, Springer-Verlag, Berlin, 1990.
• 26: G. Kuper, L. Libkin, and J. Paredaens, eds. Constraint Databases. Springer, 2000.
• 27: Leonid Libkin, Logics with counting and local properties, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.33-59, July 2000 [doi>10.1145/343369.343376]
• 28: Leonid Libkin, Elements Of Finite Model Theory (Texts in Theoretical Computer Science. An Eatcs Series), SpringerVerlag, 2004
• 29: L. Libkin. Logics over unranked trees: an overview. LMCS 2(3): (2006).
• 30: J. Lynch. Almost sure theories. Annals of Mathematical Logic, 18 (1980), 91--135.
• 31: J. Makowsky. Algorithmic aspects of the Feferman-Vaught Theorem. Annals of Pure and Applied Logic, 126 (2004), 159--213.
• 32: H. Niemisto. Locality and order-invariant logics. PhD Thesis, Univ.of Helsinki, 2007.
• 33: Frank Neven , Thomas Schwentick, Query automata over finite trees, Theoretical Computer Science, v.275 n.1-2, p.633-674, March 28 2002 [doi>10.1016/S0304-3975(01)00301-2]
• 34: J. Nurmonen. On winning strategies with unary quantifiers. Journal of Logic and Computation, 6 (1996), 779--798.
• 35: M. Otto. Two variable first-order logic over ordered domains. J. Symb. Logic 66 (2001), 685--702.
• 36: C. Papadimitriou. A note on the expressive power of Prolog. Bulletin of the EATCS, 26 (1985), 21--23.
• 37: J. Rosenstein. Linear Orderings. Academic Press, 1982.
• 38: Benjamin Rossman, On the constant-depth complexity of k-clique, Proceedings of the 40th annual ACM symposium on Theory of computing, May 17-20, 2008, Victoria, British Columbia, Canada [doi>10.1145/1374376.1374480]
• 39: Thomas Schwentick, Automata for XML---A survey, Journal of Computer and System Sciences, v.73 n.3, p.289-315, May, 2007 [doi>10.1016/j.jcss.2006.10.003]
• 40: D. Seese. Linear time computable problems and first-order descriptions. Mathematical Structures in Computer Science, 6 (1996), 505--526.
• 41: B.A. Trakhtenbrot. The impossibilty of an algorithm for the decision problem for finite models. Doklady Academii Nauk SSSR, 70 (1950), 569--572.
• 42: Moshe Y. Vardi, The complexity of relational query languages (Extended Abstract), Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.137-146, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802186]
• 43: Moshe Y. Vardi, On the complexity of bounded-variable queries (extended abstract), Proceedings of the fourteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.266-276, May 22-25, 1995, San Jose, California, United States [doi>10.1145/212433.212474]
• 44: V. Vianu. Databases and finite-model theory. In Descriptive Complexity and Finite Models, Proc. of a DIMACS workshop. AMS, 1997, pages 97--148.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Model theory

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Classes defined by grammars or automata (e.g., context-free languages, regular sets, recursive sets)

  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.4 Systems
          Subjects: Relational databases

General Terms:
Algorithms, Languages, Theory

Keywords:
complexity, expressive power, finite models, games, logics, order, query languages, types