- Authors:
-
Bonacina, Maria Paola; Moa, Johansson
- Title:
-
Interpolation systems for ground proofs in automated deduction: a survey
- Year:
-
2015
- Type of item:
-
Articolo in Rivista
- Tipologia ANVUR:
- Articolo su rivista
- Language:
-
Inglese
- Format:
-
A Stampa
- Referee:
-
Sì
- Name of journal:
- Journal of Automated Reasoning
- ISSN of journal:
- 0168-7433
- N° Volume:
-
54
- Number or Folder:
-
4
- :
- Kluwer
- Page numbers:
-
353-390
- Keyword:
-
Automated theorem proving; Satisfiability modulo theories; Superposition-based inference systems
- Short description of contents:
- Interpolation is a deductive technique applied in program analysis and verification: for example, it is used to compute over-approximations of images orrefine abstractions. An interpolation system takes a refutation and extracts an interpolant by building it inductively from partial interpolants. We survey color-based interpolation systems for ground proofs produced by key inference engines of state-of-the-art solvers: DPLL for propositional logic, equality sharing for combination of convex theories, and DPLL(T) for SMT-solving. Since color-based interpolation systems use colors to track symbols in proofs, equality is problematic, because replacement of equals by equals mixes symbols and therefore colors. We analyze interpolation in the presence of equality, and we demonstrate the color-based approach by giving a complete interpolation system for ground proofs by superposition.
- Note:
- Published online 20 March 2015
- Web page:
-
http://dx.doi.org/10.1007/s10817-015-9325-5
http://profs.sci.univr.it/~bonacina/interpolation.html
http://profs.sci.univr.it/~bonacina/worksbydate.html
http://profs.sci.univr.it/~bonacina/pub_jou.html
https://link.springer.com/article/10.1007/s10817-015-9325-5
- Product ID:
-
86268
- Handle IRIS:
-
11562/900586
- Deposited On:
-
March 3, 2015
- Last Modified:
-
November 15, 2022
- Bibliographic citation:
-
Bonacina, Maria Paola; Moa, Johansson,
Interpolation systems for ground proofs in automated deduction: a survey
«Journal of Automated Reasoning»
, vol.
54
, n.
4
,
2015
,
pp. 353-390
Consulta la scheda completa presente nel
repository istituzionale della Ricerca di Ateneo 
