Efficient Interpolant generation algorithms based on quantifier elimination: EUF, Octagons, ...
副标题：
时间：2018-07-09 来源：数学机械化重点实验室
题目： Efficient Interpolant generation algorithms based on quantifier elimination: EUF, Octagons, ...
报告人： Deepak Kapur (University of New Mexico)
时间地点： 2018.07.10 15:00pm N222
摘要： In a 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. Even though there are many algorithms reported in the literature, there is little investigation about their complexity.Interpolants generated are simple and can be efficiently represented using new symbols defined in terms of common symbols. 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. Combination methods for interpolant generation over subtheories can be developed as well. Another interesting outcome is an efficient algorithm for generating congruence closure of conditional equations.
