A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
From MaRDI portal
Publication:1247317
DOI10.1016/0022-0000(78)90021-1zbMath0381.03021OpenAlexW2008770192WikidataQ56059275 ScholiaQ56059275MaRDI QIDQ1247317
Publication date: 1978
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0022-0000(78)90021-1
Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Quantifier elimination, model completeness, and related topics (03C10)
Related Items
Decision procedures for flat array properties, On iterating linear transformations over recognizable sets of integers, Bounded model checking of infinite state systems, Short Presburger Arithmetic Is Hard, XML schema, tree logic and sheaves automata, Parallélisation sémantique, Presburger Arithmetic, Rational Generating Functions, and Quasi-Polynomials, Emptiness problems for integer circuits, Temporal Specifications with Accumulative Values, Complexity, convexity and combinations of theories, Hairpin completions and reductions: semilinearity properties, Parametric Presburger arithmetic: complexity of counting and quantifier elimination, On Presburger arithmetic extended with non-unary counting quantifiers, The complexity of the equivalence problem for two characterizations of Presburger sets, Simulation by Rounds of Letter-to-Letter Transducers, Persistence of vector replacement systems is decidable, Quantifier elimination for counting extensions of Presburger arithmetic, INTERLEAVING LOGIC AND COUNTING, Schemas for unordered XML on a DIME, Unnamed Item, Complexity results for classes of quantificational formulas, The complexity of logical theories, Tarski’s Influence on Computer Science, An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic, Undecidability of bisimilarity for Petri nets and some related problems, Target counting with Presburger constraints and its application in sensor networks, A practical approach to model checking duration calculus using Presburger arithmetic, Complexity of logical theories involving coprimality, Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols, Model-theoretic methods in combined constraint satisfiability, Unnamed Item, An Efficient Decision Procedure for Functional Decomposable Theories Based on Dual Constraints, Decidability of performance equivalence for basic parallel processes, Partial Projection of Sets Represented by Finite Automata, with Application to State-Space Visualization, Double-exponential inseparability of Robinson subsystem Q+, A complete and terminating approach to linear integer solving, Uniformly Automatic Classes of Finite Structures, Effective Quantifier Elimination for Presburger Arithmetic with Infinity, Unnamed Item, Łukasiewicz logics for cooperative games, The Value-Passing Calculus, A full first-order constraint solver for decomposable theories, From decomposable to residual theories, Unnamed Item, Decidability of bisimilarity for one-counter processes., Symbolic model checking of timed guarded commands using difference decision diagrams
Cites Work
