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 [2009/05/12 23:17] vkuncak |
sav08:quantifier_instantiation [2012/05/21 10:00] 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 $\forall x. P(x) \rightarrow Q(x)$ only if you find $P(t)$ |