Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)A new technique is presented for proving that a consequence system enjoys Craig interpolation or Maehara interpolation based on the fact that these properties hold in another consequence system. This technique is based on the existence of a back and forth translation satisfying some properties between the consequence systems. Some examples of translations satisfying those properties are described. Namely a translation between the global/local consequence systems induced by fragments of linear logic, a Kolmogorov-Gentzen-Godel style translation, and a new translation between the global consequence systems induced by full Lambek calculus and linear logic, mixing features of a Kiriyama-Ono style translation with features of a Kolmogorov-Gentzen-Godel style translation. These translations establish a strong relationship between the logics involved and are used to obtain new results about whether Craig interpolation and Maehara interpolation hold in that logics. (c) 2009 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim555515534Fundagdo para a Ciencia e a Tecnologia (FCT)EU FEDER via SQIG (Security and Quantum Information Group) at Instituto de TelecomunicacoesQuantLog [POCTI/MAT/55796/2004]QSec [PTDC/EIA/67661/2006]KLog [PTDC/MAT/68723/2006]Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)QuantLog [POCTI/MAT/55796/2004]QSec [PTDC/EIA/67661/2006]KLog [PTDC/MAT/68723/2006]FAPESP [2004/14107-2]