scientific article; zbMATH DE number 1253963
From MaRDI portal
Publication:4226937
Decidability of theories and sets of sentences (03B25) Quantifier elimination, model completeness, and related topics (03C10) Complexity of computation (including implicit computational complexity) (03D15) First-order arithmetic and fragments (03F30) Decidability and field theory (12L05) Analysis of algorithms and problem complexity (68Q25)
Recommendations
- Generic Complexity of Presburger Arithmetic
- Generic complexity of Presburger arithmetic
- Parametric Presburger arithmetic: complexity of counting and quantifier elimination
- Complexity of Presburger arithmetic with fixed quantifier dimension
- Complexity of Subcases of Presburger Arithmetic
- Complexity of short Presburger arithmetic
- New Computational Paradigms
- The complexity of pure literal elimination
- On the intrinsic complexity of elimination theory
- On the combinatorial and algebraic complexity of quantifier elimination
Cited in
(20)- Bounding quantification in parametric expansions of Presburger arithmetic
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Monadic decomposition in integer linear arithmetic
- On Presburger arithmetic extended with modulo counting quantifiers
- Effective Quantifier Elimination for Presburger Arithmetic with Infinity
- Short Presburger Arithmetic Is Hard
- Presburger arithmetic with algebraic scalar multiplications
- Presburger arithmetic with bounded quantifier alternation
- Modular inference of subprogram contracts for safety checking
- Expansions of Presburger arithmetic with the exchange property
- Quantifier elimination for counting extensions of Presburger arithmetic
- First order Büchi automata and their application to verification of LTL specifications
- Geometric decision procedures and the VC dimension of linear arithmetic theories
- An efficient quantifier elimination procedure for Presburger arithmetic
- Integer linear-exponential programming in NP by quantifier elimination
- An introduction to the theory of linear integer arithmetic (invited paper)
- Quantifier elimination for the reals with a predicate for the powers of two
- A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
- Weak quantifier elimination for the full linear theory of the integers
- Proof synthesis and reflection for linear arithmetic
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4226937)
