Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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.
 
sav08/quantifier_instantiation.txt · Last modified: 2012/05/22 14:02 by vkuncak
 
© EPFL 2018 - Legal notice