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

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

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

(35)

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

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)