Rewriting Interpolants
Christopher S. Lynch, Yuefeng Tang · Electronic Notes in Theoretical Computer Science · 2008
We give a method of constructing an interpolant for linear equality, and inequality constraints over the rational numbers. Our method is based on efficient rewriting techniques, and does not require the use of combination methods. The interpolant is constructed in such a way that it reflects the structure of the rewrite proof.