Efficient Interpolant generation algorithms based on quantifier elimination: EUF, Octagons, ...

报告人：      Deepak Kapur (University of New Mexico)

I will start with an interpolant generation algorithm in the quantifier-free theory of equality over uninterpreted symbols. Even though there are many algorithms reported in the literature, there is little investigation about their complexity.Interpolants generated are simple and can be efficiently represented using new symbols defined in terms of common symbols. This is followed by an interpolant generation algorithm for octagonal formulas, which is of complexity O(n^3), where n is the number of variables; an interpolant generated is a conjunction of octagonal formulas. Combination methods for interpolant generation over subtheories can be developed as well. Another interesting outcome is an efficient algorithm for generating congruence closure of conditional equations.