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.
EnglishSearch-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. Conflict-driven procedures perform nontrivial inferences only when resolving conflicts between formulae and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in unions of theories. It combines solvers for individual theories as theory modules within a solver for the union of the theories. In this article, we add lemma learning to CDSAT; we show that theory modules for several theories of practical interest fulfill the requirements for completeness and termination of CDSAT; and we present two ways to enrich CDSAT with proof generation. First, we present a proof-carrying CDSAT transition system that produces proof objects in memory accommodating multiple proof formats. Alternatively, we apply to CDSAT the LCF approach to proofs from interactive theorem proving, by defining a kernel of reasoning primitives that guarantees that CDSAT proofs are correct by construction.
| Titolo: | Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs | |
| Autori: | ||
| Data di pubblicazione: | 2021 | |
| Rivista: | ||
| Handle: | http://hdl.handle.net/11562/1041622 | |
| Appare nelle tipologie: | 01.01 Articolo in Rivista |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| Bonacina2021_Article_Conflict-DrivenSatisfiabilityF.pdf | Articolo principale | Versione dell'editore |  | Open Access Visualizza/Apri |
Copyright © 2021