Interpolation means finding intermediate formulae between given formulae. When formulae decorate program locations, and describe sets of program states, interpolation may enable a program analyzer to discover information about intermediate locations and states. This mechanism has an increasing number of applications, that are relevant to program analysis and synthesis. We study interpolation in theorem proving decision procedures based on the DPLL(T) paradigm. We survey interpolation systems for DPLL, equality sharing and DPLL(T), reconstructing from the literature their completeness proofs, and clarifying the requirements for interpolation in the presence of equality.
On interpolation in decision procedures
BONACINA, Maria Paola
;
2011-01-01
Abstract
Interpolation means finding intermediate formulae between given formulae. When formulae decorate program locations, and describe sets of program states, interpolation may enable a program analyzer to discover information about intermediate locations and states. This mechanism has an increasing number of applications, that are relevant to program analysis and synthesis. We study interpolation in theorem proving decision procedures based on the DPLL(T) paradigm. We survey interpolation systems for DPLL, equality sharing and DPLL(T), reconstructing from the literature their completeness proofs, and clarifying the requirements for interpolation in the presence of equality.
| File | Dimensione | Formato | |
|---|---|---|---|
|
TABLEAUX2011interpolation.pdf
accesso aperto
Descrizione: Articolo principale
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
192.1 kB
Formato
Adobe PDF
|
192.1 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
