Rewriting Interpolants

Abstract. 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.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Christopher Lynch, Yuefeng Tang
• Keywords: Efficient Rewriting Techniques, ENTCS 2008, Inequality Constraints, Linear Equality