We present a variation of Maehara's method to construct Craig-Lyndon interpolants for the three-valued propositional logic of here and there (HT), also known as Gödel's $G_3$, a superintuitionistic logic of importance in logic programming. Our method adapts a recent interpolation technique that operates on classically encoded logic programs to a variation of Mints' sequent system for HT. The approach is characterized by two stages: First, a preliminary interpolant is constructed, a formula that is an interpolant in some sense but not yet the desired HT formula. In the second stage, an actual HT interpolant is obtained from this preliminary interpolant. With the classical encoding, the preliminary interpolant is a classical Craig-Lyndon interpolant for classical encodings of the two input HT formulas. In the presented adaptation, the sequent system operates directly on HT formulas, and the preliminary interpolant is in a nonclassical logic that generalizes HT by an additional logic operator.

翻译：我们提出了一种基于Maehara方法的变体，用于为三值"此处与彼处"命题逻辑(HT)构造Craig-Lyndon插值项。HT逻辑也被称为哥德尔$G_3$逻辑，是一种在逻辑程序设计中具有重要意义的超直觉主义逻辑。该方法将一项近期提出的、可对经典编码逻辑程序进行操作的插值技术，适配到了适用于HT逻辑的Mints相继式系统变体中。该方法包含两个阶段：首先构造一个初步插值项——该公式在某种意义上是一个插值项，但还不是所需的HT公式；在第二阶段中，则从该初步插值项出发，得到实际的HT插值项。采用经典编码时，此初步插值项是输入的两个HT公式的经典编码的经典Craig-Lyndon插值项。而在本文所呈现的适配方案中，相继式系统直接对HT公式进行操作，且初步插值项处于一种通过额外逻辑算子推广了HT逻辑的非经典逻辑之中。