Abstraction-Based Satisfiability Solving of Presburger Arithmetic.

Daniel Kroening Joël Ouaknine Sanjit A. Seshia Ofer Strichman

Published in: CAV (2004)

Keyphrases

presburger arithmetic
quantifier elimination
decision procedures
algebraic structure
satisfiability problem
propositional logic
constraint propagation
relational databases
np complete
first order logic
expressive power
phase transition
automated reasoning
cardinality constraints