Skip to content

Interpolant synthesis for quadratic polynomial inequalities and combination with EUF

Citations of this article
Mendeley users who have this article in their library.
Get full text
This PDF is freely available from an open access repository. It may not have been peer-reviewed.


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, using semi-definite programming in time complexity O(n3 + nm), where n is the number of variables and m is the number of inequalities (This complexity analysis assumes that despite the numerical nature of approximate SDP algorithms, they are able to generate correct answers in a fixed number of calls.). Using the framework proposed in [22] for combining interpolants for a combination of quantifier-free theories which have their own interpolation algorithms, a combination algorithm is given for the combined theory of concave quadratic polynomial inequalities and the equality theory over uninterpreted functions (EUF).




Gan, T., Dai, L., Xia, B., Zhan, N., Kapur, D., & Chen, M. (2016). Interpolant synthesis for quadratic polynomial inequalities and combination with EUF. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9706, pp. 195–212). Springer Verlag.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free