Presburger arithmetic with bounded quantifier alternation

DOI10.1145/800133.804361MaRDI QIDQ5402572zbMATH OpenOpenAlexWikidataFDO

Authors

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

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

Recommendations

• scientific article; zbMATH DE number 1253963
• Subclasses of Presburger arithmetic and the polynomial-time hierarchy
• On Presburger arithmetic extended with modulo counting quantifiers
• Effective Quantifier Elimination for Presburger Arithmetic with Infinity
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic

Cited in

(37)

• The complexity of linear problems in fields
• Subclasses of Presburger arithmetic and the polynomial-time hierarchy
• Dominoes and the complexity of subclasses of logical theories
• Complexity, convexity and combinations of theories
• The complexity of Presburger arithmetic with bounded quantifier alternation depth
• Sentences over integral domains and their computational complexities
• A formal derivation of the decidability of the theory SA
• Complexity of Presburger arithmetic with fixed quantifier dimension
• The complexity of query evaluation in indefinite temporal constraint databases
• Bounding quantification in parametric expansions of Presburger arithmetic
• Solving quantified linear arithmetic by counterexample-guided instantiation
• A technique for proving decidability of containment and equivalence of linear constraint queries
• One-variable logic meets Presburger arithmetic
• A practical approach to model checking duration calculus using Presburger arithmetic
• Decision procedures for term algebras with integer constraints
• Temporal specifications with accumulative values
• On Presburger arithmetic extended with modulo counting quantifiers
• Complexity of Subcases of Presburger Arithmetic
• Effective Quantifier Elimination for Presburger Arithmetic with Infinity
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• scientific article; zbMATH DE number 1929303 (Why is no real title available?)
• scientific article; zbMATH DE number 3995646 (Why is no real title available?)
• Short Presburger Arithmetic Is Hard
• Presburger arithmetic with algebraic scalar multiplications
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
• On Composing Finite Forests with Modal Logics
• Expansions of Presburger arithmetic with the exchange property
• Feferman-vaught decompositions for prefix classes of first order logic
• On Presburger arithmetic extended with non-unary counting quantifiers
• An efficient quantifier elimination procedure for Presburger arithmetic
• Ehrenfeucht-Fraïssé goes automatic for real addition
• One-parametric Presburger arithmetic has quantifier elimination
• The complexity of almost linear diophantine problems
• Simple sentences that are hard to decide
• Deciding Boolean algebra with Presburger arithmetic
• A uniform method for proving lower bounds on the computational complexity of logical theories
• Proof synthesis and reflection for linear arithmetic

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

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