On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving

Abstract. Applications in software verification often require deter- mining,the satisfiability of first-order formulæ with respect to some background theories. During development, conjectures are usually false. Therefore, it is desirable to have a theorem prover that terminates on satisfiable instances. Satisfiability Modulo Theories (SMT) solvers have proven highly scalable, efficient and suitable for integrated theory rea- soning. Superposition-based inference systems are strong at reasoning with equalities, universally quantified variables, and Horn clauses. We de- scribe a calculus that tightly integrates Superposition and SMT solvers. The combination is refutationally complete if background theory sym- bols only occur in ground formulæ, and non-ground clauses are variable inactive. Termination is enforced by introducing additional axioms as hypotheses. The calculus detects any unsoundness introduced by these axioms and recovers from it.