×

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

3 Bacci, Giovanni
3 Larsen, Kim Guldstrand
2 Brauer, Jörg
2 Hansen, Mikkel
2 Janota, Mikoláš
2 King, Andy
2 Kuncak, Viktor
2 Marques-Silva, João P.
2 Reynolds, Andrew
1 Barrett, Clark W.
1 Barton, Paul I.
1 Bogomolov, Sergiy
1 Bouyer, Patricia
1 Chakraborty, Supratik
1 Cimatti, Alessandro
1 Clarke, Edmund Melson jun.
1 Deters, Morgan
1 Dvořák, Wolfgang
1 Fahrenberg, Uli
1 Forets, Marcelo
1 Frehse, Goran
1 Gläßle, Thomas
1 Griggio, Alberto
1 Järvisalo, Matti
1 John, Ajith K.
1 King, Tim
1 Klieber, William
1 Kowalewski, Stefan
1 Lagniez, Jean-Marie
1 Lonca, Emmanuel
1 Markey, Nicolas
1 Marquis, Pierre
1 Monniaux, David P.
1 Mover, Sergio
1 Podelski, Andreas
1 Reynier, Pierre-Alain
1 Roveri, Marco
1 Schilling, Christian
1 Tinelli, Cesare
1 Tonetta, Stefano
1 Wallner, Johannes Peter
1 Woltran, Stefan
all top 5

Cited in 7 Serials

4 Formal Methods in System Design
3 Artificial Intelligence
1 Journal of Optimization Theory and Applications
1 Science of Computer Programming
1 Information and Computation
1 Formal Aspects of Computing
1 Journal of Physics A: Mathematical and Theoretical
all top 5

Cited in 8 Fields

14 Computer science (68-XX)
5 Mathematical logic and foundations (03-XX)
2 Operations research, mathematical programming (90-XX)
2 Systems theory; control (93-XX)
2 Information and communication theory, circuits (94-XX)
1 Probability theory and stochastic processes (60-XX)
1 Numerical analysis (65-XX)
1 Quantum theory (81-XX)

Citations by Year