Doing logic by computer: interpolation in fragments of intuitionistic propositional logic Original Research Article

In this paper we study the interpolation property in fragments of intuitionistic and propositional logic, using both proof theoretic and semantic techniques. We will also sketch some computational methods, based on the semantical techniques introduced, to obtain counterexamples in fragment where interpolation (or the stronger property of uniform interpolation) does not hold.