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.
| Autori: | |
| Autori: | Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan |
| Presenza coautori internazionali: | sì |
| Numero degli autori: | 3 |
| Data di pubblicazione: | Being printed |
| Titolo: | Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs |
| Lingua: | Inglese |
| Supporto: | STAMPA |
| Revisione (peer review): | Esperti anonimi |
| Rivista: | JOURNAL OF AUTOMATED REASONING |
| Pagina iniziale: | 1 |
| Pagina finale: | 50 |
| Numero di pagine: | 50 |
| Parole Chiave (eng): | Lemma learning, Proof generation, Satisfiability modulo theories, Satisfiability modulo assignment |
| Abstract: | Search-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. |
| Note: | Accepted pending revision |
| Data di presentazione: | 2021-04-07T14:06:02Z |
| Appare nelle tipologie: | 01.01 Articolo in Rivista |
File in questo prodotto:
Copyright © 2021