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).
CITATION STYLE
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. https://doi.org/10.1007/978-3-319-40229-1_14
Mendeley helps you to discover research relevant for your work.