Tata Institute of Fundamental Research
Interpolation Synthesis for Quadratic Polynomial Inequalities and Combination with Theory of Equality with Uninterpreted Function Symbols (EUF)
STCS Colloquium
Speaker:
Deepak Kapur (University of New Mexico
Department of Computer Science
Albuquerque, NM 87131
United States of America)
Organiser:
N Raja
Date:
Tuesday, 22 Dec 2015, 16:00 to 17:00
Venue:
A-212 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
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.
| Speaker: | Deepak Kapur (University of New Mexico Department of Computer Science Albuquerque, NM 87131 United States of America) |
| Organiser: | N Raja |
| Date: | Tuesday, 22 Dec 2015, 16:00 to 17:00 |
| Venue: | A-212 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
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.