CATALOGO DEI PRODOTTI DELLA RICERCA
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishThe 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.
| Titolo: | Theory decision by decomposition |
| Autori: | |
| Data di pubblicazione: | 2010 |
| Rivista: | |
| Handle: | http://hdl.handle.net/11562/323520 |
| Appare nelle tipologie: | 01.01 Articolo in Rivista |
File in questo prodotto:
http://hdl.handle.net/11562/323520
Copyright © 2021