Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:quantifier_instantiation [2008/04/28 10:25] thomas.geek |
sav08:quantifier_instantiation [2009/05/12 23:17] vkuncak |
||
|---|---|---|---|
| Line 12: | Line 12: | ||
| * also incorporated in recent versions | * also incorporated in recent versions | ||
| - | Traditionally resolution-based provers have more sophisticated quantifier handling (but no decision procedures). This is changing and both approaches integrate techniques from others. | + | Traditionally resolution-based provers have more sophisticated quantifier handling (but have no decision procedures). This is changing and both approaches integrate techniques from others. |
| * [[http://www.cs.nyu.edu/~barrett/pubs/GBT07.ps|Solving Quantified Verification Conditions using Satisfiability Modulo Theories]] | * [[http://www.cs.nyu.edu/~barrett/pubs/GBT07.ps|Solving Quantified Verification Conditions using Satisfiability Modulo Theories]] | ||
| * [[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 | ||
| Line 18: | Line 18: | ||
| Recent approaches combine DPLL(T) solvers and resolution-based solvers | Recent 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 | ||
| - | |||