• English only

Differences

This shows you the differences between two versions of the page.

 sav08:quantifier_instantiation [2012/05/21 10:00]vkuncak sav08:quantifier_instantiation [2012/05/22 14:02] (current)vkuncak Both sides previous revision Previous revision 2012/05/22 14:02 vkuncak 2012/05/21 10:00 vkuncak 2012/05/21 10:00 vkuncak 2009/05/12 23:17 vkuncak 2008/04/28 10:25 thomas.geek 2008/04/24 13:15 vkuncak 2008/04/24 13:13 vkuncak created 2012/05/22 14:02 vkuncak 2012/05/21 10:00 vkuncak 2012/05/21 10:00 vkuncak 2009/05/12 23:17 vkuncak 2008/04/28 10:25 thomas.geek 2008/04/24 13:15 vkuncak 2008/04/24 13:13 vkuncak created 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.