Intuitionistic Propositional Logic with only Equivalence has no Interpolation
Lex Hendriks

Abstract:
We will show in this paper that there is no interpolation theorem for
the fragment of pure equivalence in intuitionistic propositional logic.
The computer program that was used to calculate the counterexample
by computations on a finite Kripke model is briefly sketched.