We provide elementary algorithms for two preservation theorems for first-order sentences with modulo m counting quantifiers (FO+MODm) on the class C-d of all finite structures of degree at most d: For each FO+MODm-sen...
详细信息
ISBN:
(纸本)9781450328869
We provide elementary algorithms for two preservation theorems for first-order sentences with modulo m counting quantifiers (FO+MODm) on the class C-d of all finite structures of degree at most d: For each FO+MODm-sentence that is preserved under extensions (homomorphisms) on C-d, a C-d-equivalent existential (existential-positive) FO-sentence can be constructed in 6-fold (4-fold) exponential time. For FO-sentences, the algorithm has 5-fold (4-fold) exponential time complexity. This is complemented by lower bounds showing that for FO-sentences a 3-fold exponential blow-up of the computed existential (existential-positive) sentence is unavoidable. Furthermore, we show that for an input FO-formula, a C-d-equivalent Feferman-Vaught decomposition can be computed in 3-fold exponential time. We also provide a matching lower bound.
We study the existence of Hanf normal forms for extensions FO(Q) of first-order logic by sets Q subset of P(N) of unary counting quantifiers. A formula is in Hanf normal form if it is a Boolean combination of formulas...
详细信息
ISBN:
(纸本)9781450343916
We study the existence of Hanf normal forms for extensions FO(Q) of first-order logic by sets Q subset of P(N) of unary counting quantifiers. A formula is in Hanf normal form if it is a Boolean combination of formulas zeta (x(overbar)) describing the isomorphism type of a local neighbourhood around its free variables x and statements of the form "the number of witnesses y of psi (y) belongs to (Q+k)" where Q is an element of Q, k is an element of N, and psi describes the isomorphism type of a local neighbourhood around its unique free variable y. We show that a formula from FO(Q) can be transformed into a formula in Hanf normal form that is equivalent on all structures of degree <= d if, and only if, all counting quantifiers occurring in the formula are ultimately periodic. This transformation can be carried out in worst-case optimal 3-fold exponential time. In particular, this yields an algorithmic version of Nurmonen's extension of Hanf's theorem for first-order logic with modulo-counting quantifiers. As an immediate consequence, we obtain that on finite structures of degree <= d, model checking of first-order logic with modulo-counting quantifiers is fixed-parameter tractable.
We provide elementary algorithms for two preservation theorems for first-order sentences (FO) on the class C-d of all finite structures of degree at most d: For each FO-sentence that is preserved under extensions (hom...
详细信息
We provide elementary algorithms for two preservation theorems for first-order sentences (FO) on the class C-d of all finite structures of degree at most d: For each FO-sentence that is preserved under extensions (homomorphisms) on C-d, a C-d-equivalent existential (existential-positive) FO-sentence can be constructed in 5-fold (4-fold) exponential time. This is complemented by lower bounds showing that a 3-fold exponential blow-up of the computed existential (existential-positive) sentence is unavoidable. Both algorithms can be extended (while maintaining the upper and lower bounds on their time complexity) to input first-order sentences with modulo m counting quantifiers (FO+MODm). Furthermore, we show that for an input FO-formula, a C-d-equivalent Feferman-Vaught decomposition can be computed in 3-fold exponential time. We also provide a matching lower bound.
In this article, we present a family of algorithms for linear programming based on an algorithm proposed by von Neumann. The von Neumann algorithm is very attractive due to its simplicity, but is not practical for sol...
详细信息
In this article, we present a family of algorithms for linear programming based on an algorithm proposed by von Neumann. The von Neumann algorithm is very attractive due to its simplicity, but is not practical for solving most linear programs to optimality due to its slow convergence. Our algorithms were developed with the objective of improving the practical convergence of the von Neumann algorithm while maintaining its attractive features. We present results from computational experiments on a set of linear programming problems that show significant improvements over the von Neumann algorithm.
暂无评论