EasyChair Publications
Search
Paper Information
Paper:Nikolaj Bjorner, Arie Gurfinkel, Konstantin Korovin and Ori Lahav
Instantiations, Zippers and EPR Interpolation
Title:Instantiations, Zippers and EPR Interpolation
Authors:Nikolaj Bjorner, Arie Gurfinkel, Konstantin Korovin and Ori Lahav
Keyphrases:smt, theorem proving, epr, interpolation
Paper:
Abstract:This paper describes interpolation procedures for EPR.
In principle, interpolation for EPR is simple:
It is a special case of first-order interpolation.
In practice, we would like procedures that take advantage
of properties of EPR: EPR admits finite models and those models
are sometimes possible to describe very compactly.
Inspired by procedures for propositional logic that use
models and cores, but not proofs, we develop a procedure for EPR
that uses just models and cores.
Volume:Ken Mcmillan, Aart Middeldorp, Geoff Sutcliffe and Andrei Voronkov (editors). LPAR-19. 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Series:EPiC Series in Computing
Volume number:26
Pages:35-41
Editors:Ken Mcmillan, Aart Middeldorp, Geoff Sutcliffe and Andrei Voronkov
Page views:17
Downloads:15
BibTeX entry:
@inproceedings{LPAR-19:Instantiations_Zippers_and_EPR_Interpolation,
  author    = {Nikolaj Bjorner and Arie Gurfinkel and Konstantin Korovin and Ori Lahav},
  title     = {Instantiations, Zippers and EPR Interpolation},
  booktitle = {LPAR-19. 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
  editor    = {Ken Mcmillan and Aart Middeldorp and Geoff Sutcliffe and Andrei Voronkov},
  series    = {EPiC Series in Computing},
  volume    = {26},
  pages     = {35-41},
  year      = {2014},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}