• English only

# Differences

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

Link to this comparison view

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.

sav08/quantifier_instantiation.txt · Last modified: 2012/05/22 14:02 by vkuncak

© EPFL 2018 - Legal notice