Talks and Poster Presentations (with Proceedings-Entry):

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.

English abstract:
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.

"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)

Electronic version of the publication:

Created from the Publication Database of the Vienna University of Technology.