摘要：We prove a weighted Feferman-Vaught decomposition theorem for disjoint unions and products of finite structures. The classical Feferman-Vaught Theorem describes how the evaluation of a first order sentence in a generalized product of relational structures can be reduced to the evaluation of sentences in the contributing structures and the index structure. The logic we employ for our weighted extension is based on the weighted MSO logic introduced by Droste and Gastin to obtain a Büchi-type result for weighted automata. We show that for disjoint unions and products of structures, the evaluation of formulas from two respective fragments of the logic can be reduced to the evaluation of formulas in the contributing structures. We also prove that the respective restrictions are necessary. Surprisingly, for the case of disjoint unions, the fragment is the same as the one used in the Büchi-type result of weighted automata. In fact, even the formulas used to show that the respective restrictions are necessary are the same in both cases. However, here proving that they do not allow for a Feferman-Vaught-like decomposition is more complex and employs Ramsey's Theorem. We also show how translation schemes can be applied to go beyond disjoint unions and products.
关键词：Quantitative Logic; Quantitative Model Theory; Feferman-Vaught Theorem; Translation Scheme; Transduction
