Presburger arithmetic with bounded quantifier alternation

DOI10.1145/800133.804361zbMath1282.68142OpenAlexW1969335410WikidataQ61013008 ScholiaQ61013008MaRDI QIDQ5402572

No author found.

Publication date: 14 March 2014

Published in: Proceedings of the tenth annual ACM symposium on Theory of computing - STOC '78 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/800133.804361

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70) First-order arithmetic and fragments (03F30) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (28)

A formal derivation of the decidability of the theory SA ⋮ On Composing Finite Forests with Modal Logics ⋮ Complexity of Subcases of Presburger Arithmetic ⋮ The complexity of linear problems in fields ⋮ Complexity of Presburger arithmetic with fixed quantifier dimension ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Short Presburger Arithmetic Is Hard ⋮ The complexity of query evaluation in indefinite temporal constraint databases ⋮ Subclasses of Presburger arithmetic and the polynomial-time hierarchy ⋮ Dominoes and the complexity of subclasses of logical theories ⋮ Temporal Specifications with Accumulative Values ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Complexity, convexity and combinations of theories ⋮ Feferman-vaught decompositions for prefix classes of first order logic ⋮ On Presburger arithmetic extended with non-unary counting quantifiers ⋮ Decision procedures for term algebras with integer constraints ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ The complexity of Presburger arithmetic with bounded quantifier alternation depth ⋮ A uniform method for proving lower bounds on the computational complexity of logical theories ⋮ Proof synthesis and reflection for linear arithmetic ⋮ A practical approach to model checking duration calculus using Presburger arithmetic ⋮ Ehrenfeucht-Fraïssé goes automatic for real addition ⋮ A technique for proving decidability of containment and equivalence of linear constraint queries ⋮ The complexity of almost linear diophantine problems ⋮ Effective Quantifier Elimination for Presburger Arithmetic with Infinity ⋮ Sentences over integral domains and their computational complexities ⋮ Unnamed Item ⋮ Simple sentences that are hard to decide

This page was built for publication: Presburger arithmetic with bounded quantifier alternation