We present a Maehara-style construction of Craig interpolants for the three-valued propositional logic of here and there (HT), also known as Gödel's $G_3$. The method adapts a recent interpolation technique that operates on classically encoded logic programs to a variation of a sequent calculus for HT by Mints. 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 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.

翻译：本文针对三值Here and There命题逻辑（亦称哥德尔$G_3$逻辑）提出了一种前原风格的Craig插值构造方法。该方法将近期基于经典编码逻辑程序的插值技术，适配至Mints提出的HT逻辑矢列演算变体。该方法的特征在于包含两个阶段：首先构造一个预备插值式——该公式在某种意义上是插值式，但尚未成为目标HT公式；第二阶段则从此预备插值式中导出真正的HT插值式。在经典编码框架下，预备插值式是两个输入HT公式经典编码的经典Craig插值式。而在本文提出的适配方案中，矢列系统直接对HT公式进行演算，所得预备插值式属于一种通过额外逻辑算子扩展HT的非经典逻辑。