Unsound Theorem Proving

13 years 11 months ago
Unsound Theorem Proving
Abstract. Applications in software verification often require determining 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 reasoning. Superposition-based inference systems are strong at reasoning with equalities, universally quantified variables, and Horn clauses. We describe a calculus that tightly integrates Superposition and SMT solvers. The combination is refutationally complete if background theory symbols 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.
Christopher Lynch
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CSL
Authors Christopher Lynch
Comments (0)