Algorithmic aspects of the Feferman-Vaught Theorem
Abstract:
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)