Algorithmic uses of the Feferman-Vaught theorem

DOI10.1016/J.APAL.2003.11.002MaRDI QIDQ598280zbMATH OpenOpenAlexFDO

Publication date 6 August 2004

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2003.11.002

Clique width Graph algorithms Graph polynomials Monadic second-order logic Tree width

Decidability of theories and sets of sentences (03B25) Interpolation, preservation, definability (03C40) Vertex subsets with special properties (dominating sets, independent sets, cliques, etc.) (05C69) Graph algorithms (graph-theoretic aspects) (05C85) Analysis of algorithms and problem complexity (68Q25)

Review text

The author gives a unified presentation, including new results, of how to use the Feferman-Vaught theorem, and new variations thereof, algorithmically in the case of Monadic Second-Order Logic MSOL. The introduction contains a survey of results in the considered direction. The formalism of translation schemes and its associated maps, the semantic transductions and syntactic translations are introduced. Translation schemes unify formalisms due to Tarski, Mostowski and Robinson and clarified by Rabin. A unary map between structures, the fusion, is introduced. It contracts the satisfaction set of a unary predicate to a single point. This operation satisfies a variant of the Feferman-Vaught theorem. In its full generality it is not known to be expressible as a first-order logic transduction. However, several special cases can be expressed in this way. A formalism of MSOL-inductive classes is presented. These are classes of structures built inductively using the disjoint union, quantifier-free transductions, and the fusion operation. It is shown how to construct lookup tables for reduction sequences associated with these operations, and how to use them for linear-time model checking of structures represented as parse trees of inductive classes. The author introduces graph polynomials and defines the class of MSOL-definable graph polynomials. He proves a Feferman-Vaught theorem for MSOL-definable graph polynomials, generalizes known and generates new splitting theorems for graph polynomials, and how they can be used for calculations. Finally the author discusses extensions of MSOL for which the Feferman-Vaught theorem holds as well.

Recommendations

Cites work

Cited in

(88)

This page was built for publication: Algorithmic uses of the Feferman-Vaught theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q598280)