[Back]

G. Weissenbacher:
"Interpolant Strength Revisited";
Talk: International Conference on Theory and Applications of Satisfiability Testing (SAT), Trient, Italien; 2012-06-17 - 2012-06-20; in: "International Conference on Theory and Applications of Satisfiability Testing (SAT)", LNCS / Springer, 7317 (2012), 312 - 326.

Craig´s interpolation theorem has numerous applications in model checking, au-
tomated reasoning, and synthesis. There is a variety of interpolation systems
which derive interpolants from refutation proofs; these systems are ad-hoc and
rigid in the sense that they provide exactly one interpolant for a given proof. In
previous work, we introduced a parametrised interpolation system which sub-
sumes existing interpolation methods for propositional resolution proofs and
enables the systematic variation of the logical strength and the elimination of
non-essential variables in interpolants. In this paper, we generalise this system to
propositional hyper-resolution proofs and discuss its application to proofs gener-
ated by contemporary SAT solvers. Finally, we show that, when applied to local
(or split) proofs, our extension generalises two existing interpolation systems for
first-order logic and relates them in logical strength.

http://dx.doi.org/10.1007/978-3-642-31612-8_24

http://publik.tuwien.ac.at/files/PubDat_208968.pdf