Article ID Journal Published Year Pages File Type
423605 Electronic Notes in Theoretical Computer Science 2008 14 Pages PDF
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.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics