Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Bern Switzerland, July 2011, Proceedings
Casa editrice:
Springer
ISBN:
9783642221187
Intervallo pagine:
1-16
Parole chiave:
Automated deduction; program checking; satisfiability modulo theories; equality sharing
Breve descrizione dei contenuti:
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.
Note:
Joint invited paper/talk at the Twentieth International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) and the Eighth International Workshop on First-Order Theorem Proving (FTP)
Bonacina, Maria Paola; Moa, Johansson,
On interpolation in decision proceduresAutomated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Bern Switzerland, July 2011, Proceedings
, Springer
, 2011
, pp. 1-16