INTERPOLATION IN (INTUITIONISTIC) LOGIC PROGRAMMING
D.M. Gabbay, Larisa Lvovna Maksimova · Oxford University Press eBooks · 2005
This chapter provides interpolation results for the Horn clause fragment of classical or intuitionistic logic. A weak variant of interpolation for a fragment of the intuitionistic predicate logic without disjunction and existence quantifier is proved by syntactic method. A counter-example to the general form of interpolation is given.