Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Last revision Both sides next revision | ||
sav08:quantifier_instantiation [2012/05/21 10:00] vkuncak |
sav08:quantifier_instantiation [2012/05/21 10:00] vkuncak |
||
---|---|---|---|
Line 15: | Line 15: | ||
* [[http://research.microsoft.com/projects/z3/cade07.pdf|Efficient E-matching for SMT solvers]] by Leonardo de Moura and Nikolaj Bjørner | * [[http://research.microsoft.com/projects/z3/cade07.pdf|Efficient E-matching for SMT solvers]] by Leonardo de Moura and Nikolaj Bjørner | ||
- | Recent approaches combine DPLL(T) solvers and resolution-based solvers | + | Some approaches combine DPLL(T) solvers and resolution-based solvers |
* [[http://www.mpi-inf.mpg.de/~uwe/paper/TSPASS-bibl.html|SPASS+T]] by Virgile Prevosto and Uwe Waldmann | * [[http://www.mpi-inf.mpg.de/~uwe/paper/TSPASS-bibl.html|SPASS+T]] by Virgile Prevosto and Uwe Waldmann | ||