scientific article; zbMATH DE number 1253963

zbMath0915.03032MaRDI QIDQ4226937

Volker Weispfenning

Publication date: 5 July 1999

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

Presburger Arithmeticcomplexity of quantifier eliminationupper and lower complexity bounds

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Decidability and field theory (12L05) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) First-order arithmetic and fragments (03F30) Quantifier elimination, model completeness, and related topics (03C10)

Related Items

Short Presburger Arithmetic Is Hard, Bounding quantification in parametric expansions of Presburger arithmetic, Quantifier elimination for the reals with a predicate for the powers of two, Modular inference of subprogram contracts for safety checking, A quantifier-elimination based heuristic for automatically generating inductive assertions for programs, Solving quantified linear arithmetic by counterexample-guided instantiation, Weak quantifier elimination for the full linear theory of the integers, Proof synthesis and reflection for linear arithmetic, Unnamed Item, Monadic decomposition in integer linear arithmetic