Dominoes and the complexity of subclasses of logical theories
type: Item
instance of: scholarly article
title: Dominoes and the complexity of subclasses of logical theories
zbMATH Open document ID: 0665.03027
DOI: 10.1016/0168-0072(89)90023-7
author: Erich Grädel
published in: Annals of Pure and Applied Logic
publication date: 1989-01-01T00:00:00Z
review text: The complexity of classes of quantifier prefix bounded formulas in logical theories (mainly Presburger and Skolem arithmetic) is studied. The main result for Presburger arithmetic is exponential time complexity for \(\exists \forall^*\)-formulas. Main results for Skolem arithmetic are: 1) NP-completeness of the class of \(\exists^*\)-formulas, 2) NP- completeness of the class of \(\exists\)-formulas if the divisibility relation is allowed, 3) the existence of a quantifier prefix such that the class of formulas with this prefix has exponential lower bound of time complexity. Some other theories are considered, too. The proofs are based on reduction of finite versions of the domino problems.
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 05B50
zbMATH DE Number: 4087645
zbMATH Keywords: complexity of classes of quantifier prefix bounded formulas
zbMATH Keywords: Skolem arithmetic
zbMATH Keywords: Presburger arithmetic
zbMATH Keywords: time complexity
zbMATH Keywords: NP-completeness
zbMATH Keywords: domino
MaRDI profile type: Publication
full work available at URL: 0168-0072(89)90023-7
OpenAlex ID: W1968015483
cites work: The undecidability of the domino problem
cites work: The complexity of logical theories
cites work: Q3220555
cites work: Alternation
cites work: A uniform method for proving lower bounds on the computational complexity of logical theories
cites work: Q4767716
cites work: The first order properties of products of algebraic systems
cites work: The computational complexity of logical theories
cites work: Q4082296
cites work: The complexity of Presburger arithmetic with bounded quantifier alternation depth
cites work: Q3341896
cites work: A Bound on Solutions of Linear Integer Equalities and Inequalities
cites work: Subclasses of Presburger arithmetic and the polynomial-time hierarchy
cites work: Q3795666
cites work: The decision problem for standard classes
cites work: Q3862379
cites work: ENTSCHEIDUNGSPROBLEM REDUCED TO THE AEA CASE
cites work: Q5585020
cites work: Complexity of Boolean algebras
cites work: Q3856727
cites work: Q3915990
cites work: On direct products of theories
cites work: Q3248054
cites work: Every Prime Has a Succinct Certificate
cites work: Presburger arithmetic with bounded quantifier alternation
cites work: Undecidability and nonperiodicity for tilings of the plane
cites work: Complexity of Subcases of Presburger Arithmetic
cites work: Separating Nondeterministic Time Complexity Classes
cites work: Real addition and the polynomial hierarchy
cites work: Komplexität von Entscheidungsproblemen. Ein Seminar
cites work: The polynomial-time hierarchy
cites work: Q5509685
cites work: Complete sets and the polynomial-time hierarchy
description: scientific article; zbMATH DE number 4087645