Publications

Authors:

Bonacina, Maria Paola; Moa, Johansson

Title:

On interpolation in decision procedures

Year:

2011

Type of item:

Contributo in volume (Capitolo o Saggio)

Tipologia ANVUR:

Contributo in volume (Capitolo o Saggio)

Language:

Inglese

Format:

A Stampa

Book Title:

Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Bern Switzerland, July 2011, Proceedings

Publisher:

Springer

ISBN:

9783642221187

Page numbers:

1-16

Keyword:

Automated deduction; program checking; satisfiability modulo theories; equality sharing

Short description of contents:

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)

Web page:

http://doi.org/10.1007/978-3-642-22119-4_1
https://mariapaola.github.io/

Product ID:

114334

Handle IRIS:

11562/351865

Deposited On:

October 13, 2011

Last Modified:

September 15, 2023

Bibliographic citation:

Bonacina, Maria Paola; Moa, Johansson, On interpolation in decision procedures Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Bern Switzerland, July 2011, Proceedings , Springer , 2011 , pp. 1-16

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo