On Interpolation In Decision Procedures
TABLEAUX'11: Proceedings of the 20th international conference on Automated reasoning with analytic tableaux and related methods(2011)
摘要
Interpolation means finding intermediate formulae between given formulae. When formulae decorate program locations, and describe sets of program states, interpolation may enable a program analyzer to discover information about intermediate locations and states. This mechanism has an increasing number of applications, that are relevant to program analysis and synthesis. We study interpolation in theorem proving decision procedures based on the DPLL(T) paradigm. We survey interpolation systems for DPLL, equality sharing and DPLL(T), reconstructing from the literature their completeness proofs, and clarifying the requirements for interpolation in the presence of equality.
更多查看译文
关键词
Induction Hypothesis, Decision Procedure, Congruence Class, Ground Term, Equality Sharing
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络