Theory decision by decomposition

详细信息    查看全文

• 作者：Maria Paola Bonacina ; Mnacho Echenim
• 关键词：Satisfiability modulo theories ; Decision procedures ; combination of theories ; Automated theorem proving ; Rewriting ; superposition ; paramodulation
• 刊名：Journal of Symbolic Computation
• 出版年：2010
• 出版时间：February 2010
• 年：2010
• 卷：45
• 期：2
• 页码：229-260
• 全文大小：3162 K

文摘

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 first-order 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.