Nadcházející semináře

  • Marie Turčičová (UÍ): Covariance modelling for ensemble filtering algorithms in high dimension

    27.6.2019 14:00 @ Ostatní semináře

    Seminář se koná ve čtvrtek 27. června 2019 od 14:00 v Ústavu informatiky AV ČR, v místnosti č. 222.

  • Deepak Kapur (Dept. of Computer Science, Univ. of New Mexico): Interpolant generation algorithms based on quantifier elimination

    1.7.2019 14:00 @ Hora Informaticae

    In their paper in 2006, Kapur, Majumdar and Zarba observed a connection between quantifier elimination and interpolant generation which was probably well-known but not explicitly reported in the literature on automated reasoning and formal methods. Since then I have been investigating how to develop heuristics for quantifier elimination to generate interpolants. Particularly, there is no need to have access to a proof to generate interpolants, a methodology widely used in the formal methods community. I will start with an interpolant generation algorithm in the quantifier-free theory of equality over uninterpreted symbols (EUF). This is followed by an interpolant generation algorithm for octagonal formulas, which is of complexity O(n^3), where n is the number of variables; an interpolant generated is a conjunction of octagonal formulas. Then, I will move to nonlinear (quadratic) polynomial inequalities and their combination with EUF. The key idea is that nonlinear concave quadratic polynomials can be linearized and a generalization of Motzkin's transposition theorem can be proved. Time permitting, I will discuss our recent work on using linear and nonlinear deep learning methods based on support vector machines, exploring a totally different approach for generating nonlinear interpolants from more complex formulas including transcendental functions.