Mjollnir
swMATH ID: | 38338 |
Software Authors: | Monniaux, D. |
Description: | Mjollnir: Quantifier elimination by lazy model enumeration. We propose a quantifier elimination scheme based on nested lazy model enumeration through SMT-solving, and projections. This scheme may be applied to any logic that fulfills certain conditions; we illustrate it for linear real arithmetic. The quantifier elimination problem for linear real arithmetic is doubly exponential in the worst case, and so is our method. We have implemented it and benchmarked it against other methods from the literature. |
Homepage: | https://hal.archives-ouvertes.fr/hal-00472831v2/document |
Related Software: | RAReQS; MiniSat; z3; Mathematica; Spacer; QUBE; sQueezeBF; SIMPLIFY; Yices; Chaff; SMT-LIB; Sat4j; PROPhESY; PARAM; Cmodels; Gringo; QBFLIB; QuBE++; HyComp; NuSMV |
Cited in: | 17 Documents |
all
top 5
Cited by 42 Authors
all
top 5
Cited in 7 Serials
all
top 5