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

Speaker: 

Deepak Kapur

Affiliation: 

University of New Mexico
Department of Computer Science
Albuquerque, NM 87131
United States of America

Time: 

Tuesday, 22 December 2015, 16:00 to 17:00

Venue: 

Organisers: 

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.