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. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Ge, Y., & De Moura, L. (2009). Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5643 LNCS, pp. 306–320). https://doi.org/10.1007/978-3-642-02658-4_25
Mendeley helps you to discover research relevant for your work.