Interpolation Synthesis for Quadratic Polynomial Inequalities and Combination with Theory of Equality with Uninterpreted Function Symbols (EUF)

N Raja
Tuesday, 22 Dec 2015, 16:00 to 17:00
A-212 (STCS Seminar Room)
Abstract: An algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and nonstrict) is proposed. The algorithm is based on a key observation that quadratic polynomial inequalities can be linearized if they are concave. A generalization of Motzkin's transposition theorem is proved, which is used to generate an interpolant between two mutually contradictory conjunctions of polynomial inequalities, in a way similar to the linear inequalities case.  This can be done efficiently using semi-definite programming but forsaking completeness.  A combination algorithm is given for the combined theory of concave quadratic polynomial inequalities and the equality theory over uninterpreted functions symbols using a hierarchical framework for combining interpolation algorithms for quantifier-free theories. A preliminary implementation has been explored.