Sciweavers

Share
CAV
2009
Springer

Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories

10 years 6 months ago
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
Quantifier reasoning in Satisfiability Modulo Theories (SMT) is a long-standing challenge. The practical method employed in modern SMT solvers is to instantiate quantified formulas based on heuristics, which is not refutationally complete even for pure first-order logic. We present several decidable fragments of first order logic modulo theories. We show how to construct models for satisfiable formulas in these fragments. For richer undecidable fragments, we discuss conditions under which our procedure is refutationally complete. We also describe useful heuristics based on model checking for prioritizing or avoiding instantiations.
Leonardo Mendonça de Moura, Yeting Ge
Added 25 Nov 2009
Updated 25 Nov 2009
Type Conference
Year 2009
Where CAV
Authors Leonardo Mendonça de Moura, Yeting Ge
Comments (0)
books