Algorithmic aspects of the Feferman-Vaught Theorem

J. Makowsky (Haifa) (logic seminar)


A. Tarski initiated the study of the behaviour of validity of formulas in structures when passing to substructures, forming union of chains, or other algebraic operations. The Feferman-Vaught Theorem says how the truth value of a formula of First Order Logic in a generalized product of structures depends on the factors and the index set. For generalized sums this can be extended to Monadic Second Order Logic MSOL (Laeuchli, Shelah, Gurevich). For finite structures this can be used to check MSOL properties of structures and to compute polynomial invariants (graph polynomials) of structures provided the structure was built inductively using sum-like operations. Graphs of bounded tree width and bounded clique width are built inductively using such operations. We give a precise definition of sum-like operations on structures and survey algorithmic applications in the realm of graph polynomials and link polynomials.

(Based on joint work with B. Courcelle, J. Marino, J. Przytycki, E. Ravve, and U. Rotics)