Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:quantifier_instantiation [2009/05/12 23:17] vkuncak |
sav08:quantifier_instantiation [2012/05/22 14:02] vkuncak |
||
---|---|---|---|
Line 2: | Line 2: | ||
Quantifier instantiation: | Quantifier instantiation: | ||
- | * most of the time handle quantifiers | ||
* given a conjunct $\forall x.F(x)$ and a term $t$ occurring in other conjuncts, generate $F(t)$ and continue | * given a conjunct $\forall x.F(x)$ and a term $t$ occurring in other conjuncts, generate $F(t)$ and continue | ||
* in general this is incomplete | * in general this is incomplete | ||
- | * this cannot be complete because quantified combination of linear arithmetic with uninterpreted functions symbols is highly undecidable | + | * it cannot be complete because quantified combination of linear arithmetic with uninterpreted functions symbols is highly undecidable |
- | Triggers: instantiate $\forall x. P(x) \rightarrow Q(x)$ only if you find $P(t)$ | + | Triggers: instantiate e.g. $\forall x. P(x) \rightarrow Q(x)$ only if you find $P(t)$ |
* $P(x)$ acts as a guard to limit instantiations | * $P(x)$ acts as a guard to limit instantiations | ||
* introduced in [[http://doi.acm.org/10.1145/1066100.1066102|Simplify: a theorem prover for program checking]] | * introduced in [[http://doi.acm.org/10.1145/1066100.1066102|Simplify: a theorem prover for program checking]] | ||
- | * also incorporated in recent versions | + | * user-defined trigger terms: specify terms whose instances, if present in the ground part of the formula, will lead to instantiation |
+ | * for more information see {{sav08:moskal-phd.pdf|PhD Thesis of Michal Moskal}} | ||
Traditionally resolution-based provers have more sophisticated quantifier handling (but have 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. | ||
Line 16: | Line 16: | ||
* [[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 | ||