The topic of this article is decision procedures for satisfiability modulo theories (SMT) of arbitrary quantifier-free formulae. 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.

Theory decision by decomposition

BONACINA, Maria Paola;
2010

Abstract

The topic of this article is decision procedures for satisfiability modulo theories (SMT) of arbitrary quantifier-free formulae. 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.
Satisfiability modulo theories; decision procedures; combination of theories; rewrite-based theorem proving; superposition; paramodulation
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/323520
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 14
  • ???jsp.display-item.citation.isi??? 9
social impact