Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:quantifier_instantiation [2012/05/21 10:00] vkuncak |
sav08:quantifier_instantiation [2012/05/22 14:02] (current) vkuncak |
||
|---|---|---|---|
| Line 6: | Line 6: | ||
| * it 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. | ||