Theory decision by decomposition

The topic of this article is decision procedures for satisfiability modulo theories (SMT) of arbitrary quantifier-free formulæ. We propose an approach that decomposes the formula in such a way that its definitional part, including the theory, can be compiled by a rewrite-based firstorder theorem prover, and the residual problem can be decided by an SMT-solver, based on the Davis-Putnam-Logemann-Loveland procedure. The resulting decision by stages mechanism may unite the complementary strengths of first-order provers and SMT-solvers. We demonstrate its practicality by giving decision procedures for the theories of records, integer offsets and arrays, with or without extensionality, and for combinations including such theories. Key words: Satisfiability modulo theories: decision procedures, combination of theories, Automated theorem proving: rewriting, superposition, paramodulation

• Type: Journal
• Year: 2010
• Where: JSC
• Authors: Maria Paola Bonacina, Mnacho Echenim
• Keywords: Arbitrary Quantifier-free Formulæ, Decision Procedures, JSC 2010, Satisfiability Modulo Theories