BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/641
DTSTAMP:20230914T125932Z
SUMMARY:Interpolation Synthesis for Quadratic Polynomial Inequalities and C
ombination with Theory of Equality with Uninterpreted Function Symbols (EU
F)
DESCRIPTION:Speaker: Deepak Kapur (University of New Mexico\nDepartment of
Computer Science\nAlbuquerque\, NM 87131\nUnited States of America)\n\nAbs
tract: \nAbstract: An algorithm for generating interpolants for formulas w
hich are conjunctions of quadratic polynomial inequalities (both strict an
d 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 u
sed to generate an interpolant between two mutually contradictory conjunct
ions of polynomial inequalities\, in a way similar to the linear inequalit
ies case. This can be done efficiently using semi-definite programming b
ut forsaking completeness. A combination algorithm is given for the comb
ined 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 pr
eliminary implementation has been explored.\n\n\n\n \n
URL:https://www.tcs.tifr.res.in/web/events/641
DTSTART;TZID=Asia/Kolkata:20151222T160000
DTEND;TZID=Asia/Kolkata:20151222T170000
LOCATION:A-212 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR