Sciweavers

TACAS
2009
Springer
99views Algorithms» more  TACAS 2009»
14 years 6 months ago
Ground Interpolation for the Theory of Equality
Abstract. Given a theory T and two formulas A and B jointly unsatisfiable in T , a theory interpolant of A and B is a formula I such that (i) its non-theory symbols are shared by ...
Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krsti...